Theorem syl13anc

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 \)
syl13anc.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
l2
syl3anc.3
syl3Xanc.4
l4
3jca l1 l2 _
\( \vdash \varphi \rightarrow \chi \wedge \theta \wedge \tau \)
syl13anc.5
\( \vdash \psi \wedge (\chi \wedge \theta \wedge \tau) \rightarrow \eta \)
syl2anc l0 l4 _