Theorem syl332anc 1428

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 521	. 2 ⊢ (𝜑 → (𝜎 ∧ 𝜌))
10		syl332anc.9	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌)) → 𝜇)
11	1, 2, 3, 4, 5, 6, 9, 10	syl331anc 1422	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:  mdetunilem5  22844  mdetuni0  22849  lnjatN  40661  lncmp  40664  cdlema1N  40672  4atexlemex6  40955  cdlemd4  41082  cdleme18c  41174  cdleme18d  41176  cdleme19b  41185  cdleme21ct  41210  cdleme21d  41211  cdleme21e  41212  cdleme21k  41219  cdleme22g  41229  cdleme24  41233  cdleme27a  41248  cdleme27N  41250  cdleme28a  41251  cdleme40n  41349  cdlemg16zz  41541  cdlemg37  41570  cdlemk21-2N  41772  cdlemk20-2N  41773  cdlemk28-3  41789  cdlemk19xlem  41823