Theorem syl6ci

A syllogism inference combined with contraction. (Contributed by Alan Sare, 18-Mar-2012.)

Hypotheses
syl6ci.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
syl6ci.2
\( \vdash \varphi \rightarrow \theta \)
syl6ci.3
\( \vdash \chi \rightarrow \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \tau \)
Proof
l0
syl6ci.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
syl6ci.2
l2
a1d _
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \)
syl6ci.3
\( \vdash \chi \rightarrow \theta \rightarrow \tau \)
syl6c l0 l2 _