Goal Menu:

Direct Command

The Direct 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 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.