Theorem mt4d

Modus tollens deduction. Deduction form of mt4. (Contributed by NM, 9-Jun-2006.)

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