Theorem syl2imc

A commuted version of syl2im. Implication-only version of syl2anr. (Contributed by BJ, 20-Oct-2021.)

Hypotheses
syl2im.1
\( \vdash \varphi \rightarrow \psi \)
syl2im.2
\( \vdash \chi \rightarrow \theta \)
syl2im.3
\( \vdash \psi \rightarrow \theta \rightarrow \tau \)
Conclusion
\( \vdash \chi \rightarrow \varphi \rightarrow \tau \)
Proof
l0
syl2im.1
\( \vdash \varphi \rightarrow \psi \)
l1
syl2im.2
\( \vdash \chi \rightarrow \theta \)
syl2im.3
\( \vdash \psi \rightarrow \theta \rightarrow \tau \)
syl2im l0 l1 _
com12 _