Theorem mt2

A rule similar to modus tollens. Inference associated with con2i. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Sep-2013.)

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