Theorem syl6c

Inference combining syl6 with contraction. (Contributed by Alan Sare, 2-May-2011.)

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