Theorem syl323anc 1356

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

Hypotheses

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

Assertion

Ref	Expression
syl323anc	⊢ (𝜑 → 𝜇)

Proof of Theorem syl323anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl12anc.3	. 2 ⊢ (𝜑 → 𝜃)
4		syl22anc.4	. . 3 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. . 3 ⊢ (𝜑 → 𝜂)
6	4, 5	jca 554	. 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 1350	1 ⊢ (𝜑 → 𝜇)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  4atlem11  34895  dalem52  35010  dath2  35023  dalawlem1  35157  dalaw  35172  cdlemb2  35327  4atexlem7  35361  cdleme7ga  35535  cdleme18a  35578  cdleme18c  35580  cdleme21f  35620  cdleme26f2ALTN  35652  cdleme26f2  35653  cdleme27a  35655  cdlemg17dN  35951  cdlemg18a  35966  cdlemg31d  35988  cdlemg48  36025  cdlemj1  36109  dihord4  36547