MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl33anc Structured version   Visualization version   GIF version

Theorem syl33anc 1382
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
StepHypRef Expression
1 syl3anc.1 . . 3 (𝜑𝜓)
2 syl3anc.2 . . 3 (𝜑𝜒)
3 syl3anc.3 . . 3 (𝜑𝜃)
41, 2, 33jca 1125 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl33anc.6 . 2 (𝜑𝜁)
8 syl33anc.7 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂𝜁)) → 𝜎)
94, 5, 6, 7, 8syl13anc 1369 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  initoeu2lem2  17273  mdetunilem9  21224  mdetuni0  21225  xmetrtri  22960  bl2in  23005  blhalf  23010  blssps  23029  blss  23030  blcld  23110  methaus  23125  metdstri  23454  metdscnlem  23458  metnrmlem3  23464  xlebnum  23568  pmltpclem1  24050  colinearalglem2  26699  axlowdim  26753  ssbnd  35138  totbndbnd  35139  heiborlem6  35166  2atm  36735  lplncvrlvol2  36823  dalem19  36890  paddasslem9  37036  pclclN  37099  pclfinN  37108  pclfinclN  37158  pexmidlem8N  37185  trlval3  37395  cdleme22b  37549  cdlemefr29bpre0N  37614  cdlemefr29clN  37615  cdlemefr32fvaN  37617  cdlemefr32fva1  37618  cdlemg31b0N  37902  cdlemg31b0a  37903  cdlemh  38025  dihmeetlem16N  38530  dihmeetlem18N  38532  dihmeetlem19N  38533  dihmeetlem20N  38534  hoidmvlelem1  43100
  Copyright terms: Public domain W3C validator