Theorem syl311anc
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 \)
syl23anc.5
\( \vdash \varphi \rightarrow \eta \)
syl311anc.6
\( \vdash (\psi \wedge \chi \wedge \theta) \wedge \tau \wedge \eta \rightarrow \zeta \)
Conclusion
\( \vdash \varphi \rightarrow \zeta \)
Proof
l0
syl3anc.1
l1
syl3anc.2
syl3anc.3
l3
3jca l0 l1 _
\( \vdash \varphi \rightarrow \psi \wedge \chi \wedge \theta \)
l4
syl3Xanc.4
\( \vdash \varphi \rightarrow \tau \)
l5
syl23anc.5
\( \vdash \varphi \rightarrow \eta \)
syl311anc.6
\( \vdash (\psi \wedge \chi \wedge \theta) \wedge \tau \wedge \eta \rightarrow \zeta \)
syl3anc l3 l4 l5 _