Theorem syl323anc 1427

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 521	. 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 1421	1 ⊢ (𝜑 → 𝜇)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  4atlem11  40443  dalem52  40558  dath2  40571  dalawlem1  40705  dalaw  40720  cdlemb2  40875  4atexlem7  40909  cdleme7ga  41082  cdleme18a  41125  cdleme18c  41127  cdleme21f  41166  cdleme26f2ALTN  41198  cdleme26f2  41199  cdleme27a  41201  cdlemg17dN  41497  cdlemg18a  41512  cdlemg31d  41534  cdlemg48  41571  cdlemj1  41655  dihord4  42092