Theorem con4d

Deduction associated with con4. (Contributed by NM, 26-Mar-1995.)

Hypothesis
con4d.1
\( \vdash \varphi \rightarrow \neg \psi \rightarrow \neg \chi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \rightarrow \psi \)
Proof
l0
con4d.1
\( \vdash \varphi \rightarrow \neg \psi \rightarrow \neg \chi \)
con4
\( \vdash (\neg \psi \rightarrow \neg \chi) \rightarrow \chi \rightarrow \psi \)
syl l0 _