Theorem syl332anc 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	⊢ (𝜑 → 𝜌)
syl332anc.9	⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌)) → 𝜇)

Assertion

Ref	Expression
syl332anc	⊢ (𝜑 → 𝜇)

Proof of Theorem syl332anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. 2 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
6		syl33anc.6	. 2 ⊢ (𝜑 → 𝜁)
7		syl133anc.7	. . 3 ⊢ (𝜑 → 𝜎)
8		syl233anc.8	. . 3 ⊢ (𝜑 → 𝜌)
9	7, 8	jca 511	. 2 ⊢ (𝜑 → (𝜎 ∧ 𝜌))
10		syl332anc.9	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌)) → 𝜇)
11	1, 2, 3, 4, 5, 6, 9, 10	syl331anc 1397	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:  mdetunilem5  22560  mdetuni0  22565  lnjatN  40036  lncmp  40039  cdlema1N  40047  4atexlemex6  40330  cdlemd4  40457  cdleme18c  40549  cdleme18d  40551  cdleme19b  40560  cdleme21ct  40585  cdleme21d  40586  cdleme21e  40587  cdleme21k  40594  cdleme22g  40604  cdleme24  40608  cdleme27a  40623  cdleme27N  40625  cdleme28a  40626  cdleme40n  40724  cdlemg16zz  40916  cdlemg37  40945  cdlemk21-2N  41147  cdlemk20-2N  41148  cdlemk28-3  41164  cdlemk19xlem  41198