Theorem syl3c

A syllogism inference combined with contraction. (Contributed by Alan Sare, 7-Jul-2011.)

Hypotheses
syl3c.1
\( \vdash \varphi \rightarrow \psi \)
syl3c.2
\( \vdash \varphi \rightarrow \chi \)
syl3c.3
\( \vdash \varphi \rightarrow \theta \)
syl3c.4
\( \vdash \psi \rightarrow \chi \rightarrow \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \rightarrow \tau \)
Proof
l0
syl3c.3
\( \vdash \varphi \rightarrow \theta \)
l1
syl3c.1
\( \vdash \varphi \rightarrow \psi \)
l2
syl3c.2
\( \vdash \varphi \rightarrow \chi \)
syl3c.4
\( \vdash \psi \rightarrow \chi \rightarrow \theta \rightarrow \tau \)
sylc l1 l2 _
\( \vdash \varphi \rightarrow \theta \rightarrow \tau \)
mpd l0 _