Theorem imp

Importation inference. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)

Hypothesis
imp.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
Proof
l0
df-an
\( \vdash \varphi \wedge \psi \leftrightarrow \neg (\varphi \rightarrow \neg \psi) \)
imp.1
impi _
\( \vdash \neg (\varphi \rightarrow \neg \psi) \rightarrow \chi \)
sylbi l0 _