Theorem 3syld

Triple syllogism deduction. Deduction associated with 3syld. (Contributed by Jeff Hankins, 4-Aug-2009.)

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