Theorem syl321anc 1410

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

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl33anc.6	⊢ (𝜑 → 𝜁)
syl321anc.7	⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎)

Assertion

Ref	Expression
syl321anc	⊢ (𝜑 → 𝜎)

Proof of Theorem syl321anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. 2 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. . 3 ⊢ (𝜑 → 𝜂)
6	4, 5	jca 519	. 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂))
7		syl33anc.6	. 2 ⊢ (𝜑 → 𝜁)
8		syl321anc.7	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎)
9	1, 2, 3, 6, 7, 8	syl311anc 1402	1 ⊢ (𝜑 → 𝜎)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  syl322anc  1416  cxple2ad  26767  chordthmlem3  26876  nosupbnd1lem3  27751  nosupbnd1lem4  27752  noinfbnd1lem3  27766  noinfbnd1lem4  27767  4noncolr2  40042  4noncolr1  40043  3atlem5  40075  2lplnj  40208  llnmod2i2  40451  dalawlem11  40469  dalawlem12  40470  cdleme43dN  41080  cdleme4gfv  41095  cdlemeg46nlpq  41105  cdlemg17bq  41261  cdlemg31b0N  41282  cdlemg31b0a  41283  cdlemg31c  41287  cdlemg39  41304  cdlemk47  41537  lincext3  49042