## Goal Menu:

# Direct Command

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