Theorem syl2im

Replace two antecedents. Implication-only version of syl2an. (Contributed by Wolf Lammen, 14-May-2013.)

Hypotheses
syl2im.1
\( \vdash \varphi \rightarrow \psi \)
syl2im.2
\( \vdash \chi \rightarrow \theta \)
syl2im.3
\( \vdash \psi \rightarrow \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \rightarrow \chi \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 \)
syl5 l1 _
\( \vdash \psi \rightarrow \chi \rightarrow \tau \)
syl l0 _