Theorem syl5com

Syllogism inference with commuted antecedents. (Contributed by NM, 24-May-2005.)

Hypotheses
syl5com.1
\( \vdash \varphi \rightarrow \psi \)
syl5com.2
\( \vdash \chi \rightarrow \psi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \chi \rightarrow \theta \)
Proof
syl5com.1
l1
a1d _
\( \vdash \varphi \rightarrow \chi \rightarrow \psi \)
syl5com.2
\( \vdash \chi \rightarrow \psi \rightarrow \theta \)
sylcom l1 _