Theorem syl333anc
A syllogism inference combined with contraction. (Contributed by NM,
10-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 \)
syl33anc.6
\( \vdash \varphi \rightarrow \zeta \)
syl133anc.7
\( \vdash \varphi \rightarrow \sigma \)
syl233anc.8
\( \vdash \varphi \rightarrow \rho \)
syl333anc.9
\( \vdash \varphi \rightarrow \mu \)
syl333anc.10
\( \vdash (\psi \wedge \chi \wedge \theta) \wedge (\tau \wedge \eta \wedge \zeta) \wedge (\sigma \wedge \rho \wedge \mu) \rightarrow \lambda \)
Conclusion
\( \vdash \varphi \rightarrow \lambda \)
Proof
l0
syl3anc.1
\( \vdash \varphi \rightarrow \psi \)
l1
syl3anc.2
\( \vdash \varphi \rightarrow \chi \)
l2
syl3anc.3
\( \vdash \varphi \rightarrow \theta \)
l3
syl3Xanc.4
\( \vdash \varphi \rightarrow \tau \)
l4
syl23anc.5
\( \vdash \varphi \rightarrow \eta \)
l5
syl33anc.6
\( \vdash \varphi \rightarrow \zeta \)
l6
syl133anc.7
l7
syl233anc.8
syl333anc.9
l9
3jca l6 l7 _
\( \vdash \varphi \rightarrow \sigma \wedge \rho \wedge \mu \)
syl333anc.10
\( \vdash (\psi \wedge \chi \wedge \theta) \wedge (\tau \wedge \eta \wedge \zeta) \wedge (\sigma \wedge \rho \wedge \mu) \rightarrow \lambda \)
syl331anc l0 l1 l2 l3 l4 l5 l9 _