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