Theorem mto

The rule of modus tollens. The rule says, "if \( \psi \) is not true, and \( \varphi \) implies \( \psi \), then \( \varphi \) must also be not true". Modus tollens is short for "modus tollendo tollens", a Latin phrase that means "the mode that by denying denies" - remark in [Sanford] p. 39. It is also called denying the consequent. Modus tollens is closely related to modus ponens [ax-mp]. Note that this rule is also valid in intuitionistic logic. Inference associated with con3i. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)

Hypotheses
mto.1
\( \vdash \neg \psi \)
mto.2
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \neg \varphi \)
Proof
l0
mto.2
\( \vdash \varphi \rightarrow \psi \)
mto.1
a1i _
\( \vdash \varphi \rightarrow \neg \psi \)
pm2.65i l0 _