Theorem syl322anc 1345

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl12anc.1	⊢ (𝜑 → 𝜓)
syl12anc.2	⊢ (𝜑 → 𝜒)
syl12anc.3	⊢ (𝜑 → 𝜃)
syl22anc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl33anc.6	⊢ (𝜑 → 𝜁)
syl133anc.7	⊢ (𝜑 → 𝜎)
syl322anc.8	⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌)

Assertion

Ref	Expression
syl322anc	⊢ (𝜑 → 𝜌)

Proof of Theorem syl322anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl12anc.3	. 2 ⊢ (𝜑 → 𝜃)
4		syl22anc.4	. 2 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
6		syl33anc.6	. . 3 ⊢ (𝜑 → 𝜁)
7		syl133anc.7	. . 3 ⊢ (𝜑 → 𝜎)
8	6, 7	jca 552	. 2 ⊢ (𝜑 → (𝜁 ∧ 𝜎))
9		syl322anc.8	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌)
10	1, 2, 3, 4, 5, 8, 9	syl321anc 1339	1 ⊢ (𝜑 → 𝜌)

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1030

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 195  df-an 384  df-3an 1032

This theorem is referenced by:  ax5seglem6  25532  ax5seg  25536  elpaddatriN  33910  paddasslem8  33934  paddasslem12  33938  paddasslem13  33939  pmodlem1  33953  osumcllem5N  34067  pexmidlem2N  34078  cdleme3h  34343  cdleme7ga  34356  cdleme20l  34431  cdleme21ct  34438  cdleme21d  34439  cdleme21e  34440  cdleme26e  34468  cdleme26eALTN  34470  cdleme26fALTN  34471  cdleme26f  34472  cdleme26f2ALTN  34473  cdleme26f2  34474  cdleme39n  34575  cdlemh2  34925  cdlemh  34926  cdlemk12  34959  cdlemk12u  34981  cdlemkfid1N  35030  congsub  36358  mzpcong  36360  jm2.18  36376  jm2.15nn0  36391  jm2.27c  36395