Theorem syl322anc 1425

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  cofcut2d  28196  ax5seglem6  29399  ax5seg  29403  elpaddatriN  40684  paddasslem8  40708  paddasslem12  40712  paddasslem13  40713  pmodlem1  40727  osumcllem5N  40841  pexmidlem2N  40852  cdleme3h  41116  cdleme7ga  41129  cdleme20l  41203  cdleme21ct  41210  cdleme21d  41211  cdleme21e  41212  cdleme26e  41240  cdleme26eALTN  41242  cdleme26fALTN  41243  cdleme26f  41244  cdleme26f2ALTN  41245  cdleme26f2  41246  cdleme39n  41347  cdlemh2  41697  cdlemh  41698  cdlemk12  41731  cdlemk12u  41753  cdlemkfid1N  41802  congsub  43819  mzpcong  43821  jm2.18  43837  jm2.15nn0  43852  jm2.27c  43856