Theorem syl5d

A nested syllogism deduction. Deduction associated with syl5. (Contributed by NM, 14-May-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.) (Proof shortened by Mel L. O'Cat, 2-Feb-2006.)

Hypotheses
syl5d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
syl5d.2
\( \vdash \varphi \rightarrow \theta \rightarrow \chi \rightarrow \tau \)
Conclusion
\( \vdash \varphi \rightarrow \theta \rightarrow \psi \rightarrow \tau \)
Proof
syl5d.1
l1
a1d _
\( \vdash \varphi \rightarrow \theta \rightarrow \psi \rightarrow \chi \)
syl5d.2
\( \vdash \varphi \rightarrow \theta \rightarrow \chi \rightarrow \tau \)
syldd l1 _