## Goal Menu:

# Contrapositive Command

The Contrapositive 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
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*.