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

Theorem sylan2br 476
Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)
Hypotheses
Ref Expression
sylan2br.1
sylan2br.2
Assertion
Ref Expression
sylan2br

Proof of Theorem sylan2br
StepHypRef Expression
1 sylan2br.1 . . 3
21biimpri 206 . 2
3 sylan2br.2 . 2
42, 3sylan2 474 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  syl2anbr  480  imainss  5426  funeu2  5618  imadif  5668  fnop  5689  ssimaex  5938  suppssOLD  6020  suppss2OLD  6530  tfindsg2  6696  nn0suc  6724  xpexr2  6741  extmptsuppeq  6943  suppss  6949  suppss2  6953  smores3  7043  tz7.48-2  7126  swoso  7361  isinf  7753  frfi  7785  dffi3  7911  marypha1lem  7913  ordtypelem7  7970  cnfcom2lem  8166  cnfcom2lemOLD  8174  r1pw  8284  rankxplim3  8320  dfac5  8530  cofsmo  8670  axcclem  8858  zorn2lem7  8903  wloglei  10110  divval  10234  uzind3  10981  uzind3OLD  10983  xrltnsym  11372  xaddf  11452  xrsupsslem  11527  xrinfmsslem  11528  0fz1  11734  hashunsng  12459  hashgt0elexb  12467  sumss  13546  fsumss  13547  fsumcvg3  13551  abscvgcvg  13633  isumshft  13651  geoisum1  13688  geoisum1c  13689  mertenslem2  13694  zprod  13744  prodss  13754  fprodss  13755  rpnnen2lem5  13952  gcdcllem3  14151  eulerthlem2  14312  ramcl2lem  14527  imasvscafn  14934  mreexexlem4d  15044  cycsubgcl  16227  galactghm  16428  odlem2  16563  gexlem2  16602  mulgmhm  16836  mulgghm  16837  gsumval3OLD  16908  gsumval3  16911  gsumpt  16988  gsumptOLD  16989  dprdfeq0  17062  dprdfeq0OLD  17069  srglmhm  17186  srgrmhm  17187  ringlghm  17250  ringrghm  17251  lssssr  17599  lbsind  17726  mplmonmul  18126  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  cnsubrg  18478  matplusgcell  18935  elcls  19574  neips  19614  opnnei  19621  ordtbaslem  19689  ptclsg  20116  qtopeu  20217  xmetpsmet  20851  comet  21016  metrest  21027  pcorevlem  21526  dyadmbl  22009  mbfeqalem  22049  i1fadd  22102  itg1addlem2  22104  itg2uba  22150  itgss  22218  dvcnp  22322  quotval  22688  vieta1lem2  22707  aalioulem3  22730  ulmdvlem3  22797  dvradcnv  22816  abelthlem6  22831  abelthlem9  22835  abelth  22836  logtayllem  23040  logtayl  23041  cxpcl  23055  recxpcl  23056  cxpcn3lem  23121  leibpi  23273  musum  23467  dchrelbas3  23513  sumdchr2  23545  lgscllem  23578  lgsdir2  23603  dchrvmasumiflem2  23687  rpvmasum2  23697  padicabv  23815  padicabvf  23816  padicabvcxp  23817  nmooval  25678  hiidge0  26015  hommval  26655  hfmmval  26658  nmcfnlbi  26971  mdslmd1i  27248  mdslmd3i  27251  sumdmdlem2  27338  foresf1o  27403  disjdifprg  27436  suppss2f  27477  cnvoprab  27546  xdivval  27615  esumfsupre  28077  dya2iocnei  28253  eulerpartlemgc  28301  eulerpartlemb  28307  eulerpartlemgh  28317  ballotlemfc0  28431  ballotlemfcc  28432  subfacp1lem5  28628  subfacp1lem6  28629  cvmliftlem10  28739  elmrsubrn  28880  wfr3g  29342  tfr3ALT  29365  colinearperm1  29712  colinearperm5  29716  endofsegid  29735  segcon2  29755  seglecgr12im  29760  segletr  29764  colinbtwnle  29768  broutsideof2  29772  btwnoutside  29775  outsideoftr  29779  outsidele  29782  opnbnd  30143  heibor1lem  30305  heiborlem3  30309  heiborlem10  30316  ablo4pnp  30342  crngm4  30400  sdrgacs  31150  cntzsdrg  31151  dvgrat  31193  radcnvrat  31195  lcmgcd  31213  lcmdvds  31214  cncfiooicclem1  31696  fourierdlem101  31990  etransclem24  32041  lkrpssN  34888  pclvalN  35614  polvalN  35629  lclkrlem2x  37257  hgmaprnlem5N  37630
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
  Copyright terms: Public domain W3C validator