Theorem mtod

Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)

Hypotheses
mtod.1
\( \vdash \varphi \rightarrow \neg \chi \)
mtod.2
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \neg \psi \)
Proof
l0
mtod.2
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
mtod.1
a1d _
\( \vdash \varphi \rightarrow \psi \rightarrow \neg \chi \)
pm2.65d l0 _