Theorem sylsyld

A double syllogism inference. (Contributed by Alan Sare, 20-Apr-2011.)

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