Theorem sylcom

Syllogism inference with commutation of antecedents. (Contributed by NM, 29-Aug-2004.) (Proof shortened by Mel L. O'Cat, 2-Feb-2006.) (Proof shortened by Stefan Allan, 23-Feb-2006.)

Hypotheses
sylcom.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
sylcom.2
\( \vdash \psi \rightarrow \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \)
Proof
l0
sylcom.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
sylcom.2
a2i _
\( \vdash (\psi \rightarrow \chi) \rightarrow \psi \rightarrow \theta \)
syl l0 _