MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl23anc Unicode version

Theorem syl23anc 1235
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1
sylXanc.2
sylXanc.3
sylXanc.4
sylXanc.5
syl23anc.6
Assertion
Ref Expression
syl23anc

Proof of Theorem syl23anc
StepHypRef Expression
1 sylXanc.1 . . 3
2 sylXanc.2 . . 3
31, 2jca 532 . 2
4 sylXanc.3 . 2
5 sylXanc.4 . 2
6 sylXanc.5 . 2
7 syl23anc.6 . 2
83, 4, 5, 6, 7syl13anc 1230 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  suppofss1d  6956  suppofss2d  6957  cnfcomlem  8164  cnfcomlemOLD  8172  ackbij1lem16  8636  div2subd  10395  symg2bas  16423  evl1expd  18381  psgndiflemA  18637  oftpos  18954  restopn2  19678  tsmsxp  20657  blcld  21008  metustexhalfOLD  21066  metustexhalf  21067  cnllycmp  21456  dvlipcn  22395  tanregt0  22926  ostthlem1  23812  ax5seglem6  24237  axcontlem4  24270  axcontlem7  24273  wwlkextwrd  24728  pnfneige0  27933  qqhval2  27963  esumcocn  28086  heiborlem8  30314  mpaaeu  31099  bnj1125  34048  2atjm  35169  1cvrat  35200  lvolnlelln  35308  lvolnlelpln  35309  4atlem3  35320  lplncvrlvol  35340  dalem39  35435  cdleme4a  35964  cdleme15  36003  cdleme16c  36005  cdleme19b  36030  cdleme19e  36033  cdleme20d  36038  cdleme20g  36041  cdleme20j  36044  cdleme20k  36045  cdleme20l2  36047  cdleme20l  36048  cdleme20m  36049  cdleme22e  36070  cdleme22eALTN  36071  cdleme22f  36072  cdleme27cl  36092  cdlemefr27cl  36129
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 185  df-an 371  df-3an 975
  Copyright terms: Public domain W3C validator