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