Goal Menu:

Contrapositive Command

The Contrapositive 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 Contrapositive command, then Proof Designer will create a subproof in which it is assumed that Q is false, and it will say that to complete the subproof you must prove ¬P.