Theorem mt2d

Modus tollens deduction. (Contributed by NM, 4-Jul-1994.)

Hypotheses
mt2d.1
\( \vdash \varphi \rightarrow \chi \)
mt2d.2
\( \vdash \varphi \rightarrow \psi \rightarrow \neg \chi \)
Conclusion
\( \vdash \varphi \rightarrow \neg \psi \)
Proof
l0
mt2d.1
\( \vdash \varphi \rightarrow \chi \)
mt2d.2
con2d _
\( \vdash \varphi \rightarrow \chi \rightarrow \neg \psi \)
mpd l0 _