Theorem syl121anc

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

Hypotheses
syl3anc.1
\( \vdash \varphi \rightarrow \psi \)
syl3anc.2
\( \vdash \varphi \rightarrow \chi \)
syl3anc.3
\( \vdash \varphi \rightarrow \theta \)
syl3Xanc.4
\( \vdash \varphi \rightarrow \tau \)
syl121anc.5
\( \vdash \psi \wedge \chi \wedge \theta \wedge \tau \rightarrow \eta \)
Conclusion
\( \vdash \varphi \rightarrow \eta \)
Proof
l0
syl3anc.1
\( \vdash \varphi \rightarrow \psi \)
l1
syl3anc.2
syl3anc.3
l3
jca l1 _
\( \vdash \varphi \rightarrow \chi \wedge \theta \)
l4
syl3Xanc.4
\( \vdash \varphi \rightarrow \tau \)
syl121anc.5
\( \vdash \psi \wedge \chi \wedge \theta \wedge \tau \rightarrow \eta \)
syl3anc l0 l3 l4 _