Theorem syl322anc 1397

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	⊢ (𝜑 → 𝜎)
syl322anc.8	⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌)

Assertion

Ref	Expression
syl322anc	⊢ (𝜑 → 𝜌)

Proof of Theorem syl322anc

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	. . 3 ⊢ (𝜑 → 𝜁)
7		syl133anc.7	. . 3 ⊢ (𝜑 → 𝜎)
8	6, 7	jca 512	. 2 ⊢ (𝜑 → (𝜁 ∧ 𝜎))
9		syl322anc.8	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌)
10	1, 2, 3, 4, 5, 8, 9	syl321anc 1391	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:  ax5seglem6  27302  ax5seg  27306  elpaddatriN  37817  paddasslem8  37841  paddasslem12  37845  paddasslem13  37846  pmodlem1  37860  osumcllem5N  37974  pexmidlem2N  37985  cdleme3h  38249  cdleme7ga  38262  cdleme20l  38336  cdleme21ct  38343  cdleme21d  38344  cdleme21e  38345  cdleme26e  38373  cdleme26eALTN  38375  cdleme26fALTN  38376  cdleme26f  38377  cdleme26f2ALTN  38378  cdleme26f2  38379  cdleme39n  38480  cdlemh2  38830  cdlemh  38831  cdlemk12  38864  cdlemk12u  38886  cdlemkfid1N  38935  congsub  40792  mzpcong  40794  jm2.18  40810  jm2.15nn0  40825  jm2.27c  40829