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

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

Proof of Theorem syl211anc
StepHypRef Expression
1 sylXanc.1 . . 3
2 sylXanc.2 . . 3
31, 2jca 532 . 2
4 sylXanc.3 . 2
5 sylXanc.4 . 2
6 syl211anc.5 . 2
73, 4, 5, 6syl3anc 1228 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369  /\w3a 973 This theorem is referenced by:  syl212anc  1238  syl221anc  1239  supicc  11697  modaddmulmod  12053  limsupgre  13304  limsupbnd1  13305  limsupbnd2  13306  lbspss  17728  lindff1  18855  islinds4  18870  mdetunilem9  19122  madutpos  19144  neiptopnei  19633  mbflimsup  22073  cxpneg  23062  cxpmul2  23070  cxpsqrt  23084  cxpaddd  23098  cxpsubd  23099  divcxpd  23103  fsumharmonic  23341  bposlem1  23559  chpchtlim  23664  ax5seg  24241  archiabllem2c  27739  mullimc  31622  mullimcf  31629  usgra2pthspth  32351  lincfsuppcl  33014  lshpnelb  34709  cdlemg2fv2  36326  cdlemg2m  36330  cdlemg9a  36358  cdlemg9b  36359  cdlemg12b  36370  cdlemg14f  36379  cdlemg14g  36380  cdlemg17dN  36389  cdlemkj  36589  cdlemkuv2  36593  cdlemk52  36680  cdlemk53a  36681 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