Theorem syl6d

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

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