Theorem syl321anc 1394

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 511	. 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂))
7		syl33anc.6	. 2 ⊢ (𝜑 → 𝜁)
8		syl321anc.7	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎)
9	1, 2, 3, 6, 7, 8	syl311anc 1386	1 ⊢ (𝜑 → 𝜎)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  syl322anc  1400  cxple2ad  26690  chordthmlem3  26800  nosupbnd1lem3  27678  nosupbnd1lem4  27679  noinfbnd1lem3  27693  noinfbnd1lem4  27694  4noncolr2  39714  4noncolr1  39715  3atlem5  39747  2lplnj  39880  llnmod2i2  40123  dalawlem11  40141  dalawlem12  40142  cdleme43dN  40752  cdleme4gfv  40767  cdlemeg46nlpq  40777  cdlemg17bq  40933  cdlemg31b0N  40954  cdlemg31b0a  40955  cdlemg31c  40959  cdlemg39  40976  cdlemk47  41209  lincext3  48702