## 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
.