Theorem syl33anc 1385

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	⊢ (𝜑 → 𝜁)
syl33anc.7	⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎)

Assertion

Ref	Expression
syl33anc	⊢ (𝜑 → 𝜎)

Proof of Theorem syl33anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	3jca 1128	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl33anc.6	. 2 ⊢ (𝜑 → 𝜁)
8		syl33anc.7	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎)
9	4, 5, 6, 7, 8	syl13anc 1372	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:  xpord3inddlem  8139  initoeu2lem2  17964  mdetunilem9  22121  mdetuni0  22122  xmetrtri  23860  bl2in  23905  blhalf  23910  blssps  23929  blss  23930  blcld  24013  methaus  24028  metdstri  24366  metdscnlem  24370  metnrmlem3  24376  xlebnum  24480  pmltpclem1  24964  colinearalglem2  28162  axlowdim  28216  ssbnd  36651  totbndbnd  36652  heiborlem6  36679  2atm  38393  lplncvrlvol2  38481  dalem19  38548  paddasslem9  38694  pclclN  38757  pclfinN  38766  pclfinclN  38816  pexmidlem8N  38843  trlval3  39053  cdleme22b  39207  cdlemefr29bpre0N  39272  cdlemefr29clN  39273  cdlemefr32fvaN  39275  cdlemefr32fva1  39276  cdlemg31b0N  39560  cdlemg31b0a  39561  cdlemh  39683  dihmeetlem16N  40188  dihmeetlem18N  40190  dihmeetlem19N  40191  dihmeetlem20N  40192  hoidmvlelem1  45301