Theorem syl322anc 1398

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 1392	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:  cofcut2d  27285  ax5seglem6  27946  ax5seg  27950  elpaddatriN  38339  paddasslem8  38363  paddasslem12  38367  paddasslem13  38368  pmodlem1  38382  osumcllem5N  38496  pexmidlem2N  38507  cdleme3h  38771  cdleme7ga  38784  cdleme20l  38858  cdleme21ct  38865  cdleme21d  38866  cdleme21e  38867  cdleme26e  38895  cdleme26eALTN  38897  cdleme26fALTN  38898  cdleme26f  38899  cdleme26f2ALTN  38900  cdleme26f2  38901  cdleme39n  39002  cdlemh2  39352  cdlemh  39353  cdlemk12  39386  cdlemk12u  39408  cdlemkfid1N  39457  congsub  41352  mzpcong  41354  jm2.18  41370  jm2.15nn0  41385  jm2.27c  41389