Theorem con1d

A contraposition deduction. (Contributed by NM, 27-Dec-1992.)

Hypothesis
con1d.1
\( \vdash \varphi \rightarrow \neg \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \neg \chi \rightarrow \psi \)
Proof
l0
con1d.1
\( \vdash \varphi \rightarrow \neg \psi \rightarrow \chi \)
notnot
\( \vdash \chi \rightarrow \neg \neg \chi \)
syl6 l0 _
con4d _