Theorem syl10

A nested syllogism inference. (Contributed by Alan Sare, 17-Jul-2011.)

Hypotheses
syl10.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
syl10.2
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \rightarrow \tau \)
syl10.3
\( \vdash \chi \rightarrow \tau \rightarrow \eta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \rightarrow \eta \)
Proof
l0
syl10.2
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \rightarrow \tau \)
l1
syl10.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
syl10.3
\( \vdash \chi \rightarrow \tau \rightarrow \eta \)
syl6 l1 _
\( \vdash \varphi \rightarrow \psi \rightarrow \tau \rightarrow \eta \)
syldd l0 _