Theorem syl233anc
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 \)
syl33anc.6
\( \vdash \varphi \rightarrow \zeta \)
syl133anc.7
\( \vdash \varphi \rightarrow \sigma \)
syl233anc.8
\( \vdash \varphi \rightarrow \rho \)
syl233anc.9
\( \vdash \psi \wedge \chi \wedge (\theta \wedge \tau \wedge \eta) \wedge (\zeta \wedge \sigma \wedge \rho) \rightarrow \mu \)
Conclusion
\( \vdash \varphi \rightarrow \mu \)
Proof
l0
syl3anc.1
syl3anc.2
l2
jca l0 _
\( \vdash \varphi \rightarrow \psi \wedge \chi \)
l3
syl3anc.3
\( \vdash \varphi \rightarrow \theta \)
l4
syl3Xanc.4
\( \vdash \varphi \rightarrow \tau \)
l5
syl23anc.5
\( \vdash \varphi \rightarrow \eta \)
l6
syl33anc.6
\( \vdash \varphi \rightarrow \zeta \)
l7
syl133anc.7
\( \vdash \varphi \rightarrow \sigma \)
l8
syl233anc.8
\( \vdash \varphi \rightarrow \rho \)
syl233anc.9
\( \vdash \psi \wedge \chi \wedge (\theta \wedge \tau \wedge \eta) \wedge (\zeta \wedge \sigma \wedge \rho) \rightarrow \mu \)
syl133anc l2 l3 l4 l5 l6 l7 l8 _