Theorem expdcom

Commuted form of expd. (Contributed by Alan Sare, 18-Mar-2012.) Shorten expd. (Revised by Wolf Lammen, 28-Jul-2022.)

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