Theorem syldd

Nested syllogism deduction. Deduction associated with syld. Double deduction associated with syl. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 11-May-2013.)

Hypotheses
syldd.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
syldd.2
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \tau \)
Proof
l0
syldd.2
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \rightarrow \tau \)
l1
syldd.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
imim2
\( \vdash (\theta \rightarrow \tau) \rightarrow (\chi \rightarrow \theta) \rightarrow \chi \rightarrow \tau \)
syl6c l0 l1 _