Theorem ex

Exportation inference. (This theorem used to be labeled "exp" but was changed to "ex" so as not to conflict with the math token "exp", per the June 2006 Metamath spec change.) A translation of natural deduction rule -> I ( -> introduction), see [natded]. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)

Hypothesis
ex.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Proof
l0
df-an
\( \vdash \varphi \wedge \psi \leftrightarrow \neg (\varphi \rightarrow \neg \psi) \)
ex.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
sylbir l0 _
expi _