If you have givens of the forms *P*
and *P*→*Q*, then you may infer
*Q*. Select the givens and give the Modus Ponens command, and Proof
Designer will make the inference.

You can also use this command to work backwards from your goal. If you
have a given of the form *P*→*Q*
and your goal is *Q*, then you could complete the proof by first
proving *P* and then using modus ponens to infer *Q* from
*P* and *P*→*Q*. If you
want to do this, select the given *P*→*Q* and the goal
*Q* and give the Modus Ponens
command. Proof Designer will say that you now have to prove *P*, and
it will say that once *P* has been proven, it can be used, together
with *P*→*Q*, to infer *Q*.