Theorem con3d

A contraposition deduction. Deduction form of con3. (Contributed by NM, 10-Jan-1993.)

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