Q and 
Q, then
you may infer P. Select the givens
and give the Modus Tollens command, and Proof Designer will make the
inference.
If you have givens of the forms PQ and Q, then
you may infer P. Select the givens
and give the Modus Tollens 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 P, then you could
complete the proof by first proving Q and then using modus tollens to infer P from PQ and Q. If
you want to do this, select the given PQ and the goal P and give the Modus Tollens command. Proof Designer
will say that you now have to prove Q, and it will say that once Q has been proven, it can be used, together with
PQ, to infer P.