Theorem syl11

A syllogism inference. Commuted form of an instance of syl. (Contributed by BJ, 25-Oct-2021.)

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