Theorem mt3d

Modus tollens deduction. (Contributed by NM, 26-Mar-1995.)

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