Theorem syl21anc

Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)

Hypotheses
syl12anc.1
\( \vdash \varphi \rightarrow \psi \)
syl12anc.2
\( \vdash \varphi \rightarrow \chi \)
syl12anc.3
\( \vdash \varphi \rightarrow \theta \)
syl21anc.4
\( \vdash \psi \wedge \chi \wedge \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \rightarrow \tau \)
Proof
l0
syl12anc.1
syl12anc.2
l2
jca l0 _
\( \vdash \varphi \rightarrow \psi \wedge \chi \)
l3
syl12anc.3
\( \vdash \varphi \rightarrow \theta \)
syl21anc.4
\( \vdash \psi \wedge \chi \wedge \theta \rightarrow \tau \)
syl2anc l2 l3 _