Theorem syl332anc 1400

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 512	. 2 ⊢ (𝜑 → (𝜎 ∧ 𝜌))
10		syl332anc.9	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌)) → 𝜇)
11	1, 2, 3, 4, 5, 6, 9, 10	syl331anc 1394	1 ⊢ (𝜑 → 𝜇)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  mdetunilem5  21765  mdetuni0  21770  lnjatN  37794  lncmp  37797  cdlema1N  37805  4atexlemex6  38088  cdlemd4  38215  cdleme18c  38307  cdleme18d  38309  cdleme19b  38318  cdleme21ct  38343  cdleme21d  38344  cdleme21e  38345  cdleme21k  38352  cdleme22g  38362  cdleme24  38366  cdleme27a  38381  cdleme27N  38383  cdleme28a  38384  cdleme40n  38482  cdlemg16zz  38674  cdlemg37  38703  cdlemk21-2N  38905  cdlemk20-2N  38906  cdlemk28-3  38922  cdlemk19xlem  38956