Theorem con2d

A contraposition deduction. (Contributed by NM, 19-Aug-1993.)

Hypothesis
con2d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \neg \chi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \rightarrow \neg \psi \)
Proof
l0
notnotr
\( \vdash \neg \neg \psi \rightarrow \psi \)
con2d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \neg \chi \)
syl5 l0 _
con4d _