Theorem syl12anc

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 \)
syl12anc.4
\( \vdash \psi \wedge (\chi \wedge \theta) \rightarrow \tau \)
Conclusion
\( \vdash \varphi \rightarrow \tau \)
Proof
l0
syl12anc.1
\( \vdash \varphi \rightarrow \psi \)
l1
syl12anc.2
syl12anc.3
l3
jca l1 _
\( \vdash \varphi \rightarrow \chi \wedge \theta \)
syl12anc.4
\( \vdash \psi \wedge (\chi \wedge \theta) \rightarrow \tau \)
syl2anc l0 l3 _