Theorem syl22anc

Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

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