Theorem syl323anc 1403

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 1397	1 ⊢ (𝜑 → 𝜇)

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

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 1089

This theorem is referenced by:  4atlem11  39982  dalem52  40097  dath2  40110  dalawlem1  40244  dalaw  40259  cdlemb2  40414  4atexlem7  40448  cdleme7ga  40621  cdleme18a  40664  cdleme18c  40666  cdleme21f  40705  cdleme26f2ALTN  40737  cdleme26f2  40738  cdleme27a  40740  cdlemg17dN  41036  cdlemg18a  41051  cdlemg31d  41073  cdlemg48  41110  cdlemj1  41194  dihord4  41631