Theorem expcom

Exportation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)

Hypothesis
ex.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
Conclusion
\( \vdash \psi \rightarrow \varphi \rightarrow \chi \)
Proof
ex.1
ex _
com12 _