Theorem con3dimp

Variant of con3d with importation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis
con3dimp.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \wedge \neg \chi \rightarrow \neg \psi \)
Proof
con3dimp.1
con3d _
imp _