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  40803  dalem52  40918  dath2  40931  dalawlem1  41065  dalaw  41080  cdlemb2  41235  4atexlem7  41269  cdleme7ga  41442  cdleme18a  41485  cdleme18c  41487  cdleme21f  41526  cdleme26f2ALTN  41558  cdleme26f2  41559  cdleme27a  41561  cdlemg17dN  41857  cdlemg18a  41872  cdlemg31d  41894  cdlemg48  41931  cdlemj1  42015  dihord4  42452