Strategy Menu:

Biconditional Command

The Biconditional command can only be used when you have a goal of the form PQ. 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 PQ and one for the proof of QP. The two subproofs are labeled with the symbols and , representing the two directions of the biconditional symbol .