Infer Menu:

Modus Ponens Command

If you have givens of the forms P and PQ, 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 PQ 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 PQ. If you want to do this, select the given PQ 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 PQ, to infer Q.