Theorem syl6com

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

Hypotheses
syl6com.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
syl6com.2
\( \vdash \chi \rightarrow \theta \)
Conclusion
\( \vdash \psi \rightarrow \varphi \rightarrow \theta \)
Proof
l0
syl6com.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
syl6com.2
\( \vdash \chi \rightarrow \theta \)
syl6 l0 _
com12 _