Theorem syl332anc 1401

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

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

This theorem is referenced by:  mdetunilem5  22125  mdetuni0  22130  lnjatN  38737  lncmp  38740  cdlema1N  38748  4atexlemex6  39031  cdlemd4  39158  cdleme18c  39250  cdleme18d  39252  cdleme19b  39261  cdleme21ct  39286  cdleme21d  39287  cdleme21e  39288  cdleme21k  39295  cdleme22g  39305  cdleme24  39309  cdleme27a  39324  cdleme27N  39326  cdleme28a  39327  cdleme40n  39425  cdlemg16zz  39617  cdlemg37  39646  cdlemk21-2N  39848  cdlemk20-2N  39849  cdlemk28-3  39865  cdlemk19xlem  39899