Theorem syl323anc 1401

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

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl33anc.6	⊢ (𝜑 → 𝜁)
syl133anc.7	⊢ (𝜑 → 𝜎)
syl233anc.8	⊢ (𝜑 → 𝜌)
syl323anc.9	⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) → 𝜇)

Assertion

Ref	Expression
syl323anc	⊢ (𝜑 → 𝜇)

Proof of Theorem syl323anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. 2 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. . 3 ⊢ (𝜑 → 𝜂)
6	4, 5	jca 511	. 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂))
7		syl33anc.6	. 2 ⊢ (𝜑 → 𝜁)
8		syl133anc.7	. 2 ⊢ (𝜑 → 𝜎)
9		syl233anc.8	. 2 ⊢ (𝜑 → 𝜌)
10		syl323anc.9	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) → 𝜇)
11	1, 2, 3, 6, 7, 8, 9, 10	syl313anc 1395	1 ⊢ (𝜑 → 𝜇)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  4atlem11  39612  dalem52  39727  dath2  39740  dalawlem1  39874  dalaw  39889  cdlemb2  40044  4atexlem7  40078  cdleme7ga  40251  cdleme18a  40294  cdleme18c  40296  cdleme21f  40335  cdleme26f2ALTN  40367  cdleme26f2  40368  cdleme27a  40370  cdlemg17dN  40666  cdlemg18a  40681  cdlemg31d  40703  cdlemg48  40740  cdlemj1  40824  dihord4  41261