## Strategy Menu:

# Biconditional Command

The Biconditional command can only be used when you
have a goal of the form *P*↔*Q*.
If you select a goal of this form and give the Biconditional command, then
Proof Designer will create two subproofs, one for the proof of
*P*→*Q* and one for the proof of
*Q*→*P*. The two subproofs are labeled with
the symbols → and ←, representing the two directions of the biconditional symbol
↔.