Theorem syl322anc 1518

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 508	. 2 ⊢ (𝜑 → (𝜁 ∧ 𝜎))
9		syl322anc.8	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌)
10	1, 2, 3, 4, 5, 8, 9	syl321anc 1512	1 ⊢ (𝜑 → 𝜌)

Syntax hints:   → wi 4   ∧ wa 385   ∧ w3a 1108

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 199  df-an 386  df-3an 1110

This theorem is referenced by:  ax5seglem6  26175  ax5seg  26179  elpaddatriN  35828  paddasslem8  35852  paddasslem12  35856  paddasslem13  35857  pmodlem1  35871  osumcllem5N  35985  pexmidlem2N  35996  cdleme3h  36260  cdleme7ga  36273  cdleme20l  36347  cdleme21ct  36354  cdleme21d  36355  cdleme21e  36356  cdleme26e  36384  cdleme26eALTN  36386  cdleme26fALTN  36387  cdleme26f  36388  cdleme26f2ALTN  36389  cdleme26f2  36390  cdleme39n  36491  cdlemh2  36841  cdlemh  36842  cdlemk12  36875  cdlemk12u  36897  cdlemkfid1N  36946  congsub  38326  mzpcong  38328  jm2.18  38344  jm2.15nn0  38359  jm2.27c  38363