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

Theorem simpr2 1003
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
Assertion
Ref Expression
simpr2

Proof of Theorem simpr2
StepHypRef Expression
1 simp2 997 . 2
21adantl 466 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  simplr2  1039  simprr2  1045  simp1r2  1093  simp2r2  1099  simp3r2  1105  3anandis  1330  wereu  4880  isopolem  6241  fr3nr  6615  frfi  7785  intrnfi  7896  fisupcl  7948  cnfcomlem  8164  cnfcomlemOLD  8172  ackbij1lem15  8635  cofsmo  8670  sornom  8678  fpwwe2lem5  9033  dedekindle  9766  supmul1  10533  eluzuzle  11118  xlesubadd  11484  elioc2  11616  elico2  11617  elicc2  11618  fseq1p1m1  11781  fz0fzelfz0  11809  swrdsymbeq  12672  ccatswrd  12681  swrdswrdlem  12684  tanadd  13902  dvds2ln  14014  cshwsidrepsw  14578  ressress  14694  f1ovscpbl  14923  mreexexlem4d  15044  mreexexd  15045  iscatd2  15078  2oppccomf  15120  issubc3  15218  fthmon  15296  fuccocl  15333  fucidcl  15334  invfuc  15343  curf2cl  15500  yonedalem4c  15546  yonedalem3  15549  pospo  15603  latjle12  15692  latjlej1  15695  latnlej2  15701  latlem12  15708  latmlem1  15711  latledi  15719  latjass  15725  latj12  15726  latj32  15727  latj13  15728  latj31  15729  latjrot  15730  latjjdi  15733  latjjdir  15734  latdisdlem  15819  prdsmndd  15953  frmdmnd  16027  grpsubrcan  16119  grpsubadd  16126  grpaddsubass  16128  grpsubsub4  16131  grppnpcan2  16132  grpnpncan  16133  mulgnndir  16164  mulgnn0dir  16165  mulgdir  16167  mulgnnass  16170  mulgnn0ass  16171  mulgass  16172  mulgsubdir  16173  pwsmulg  16184  issubg2  16216  eqgval  16250  qusgrp  16256  galcan  16342  gacan  16343  oppgmnd  16389  symggrp  16425  fvcosymgeq  16454  pmtrprfv  16478  psgnunilem3  16521  cmn32  16816  cmn12  16818  abladdsub  16825  mulgdi  16835  mulgsubdi  16838  dprdss  17076  dprdz  17077  dprdf1o  17079  dprdsn  17083  dprd2da  17091  dmdprdsplit  17096  ablfac1b  17121  pgpfac1lem5  17130  srgi  17163  srgbinom  17196  ringi  17211  prdsringd  17261  opprring  17280  mulgass3  17286  dvrass  17339  subrgunit  17447  issubrg2  17449  abvdiv  17486  lsssn0  17594  islss3  17605  prdslmodd  17615  islmhm2  17684  lspsolv  17789  islbs2  17800  islbs3  17801  lbsextlem4  17807  sralmod  17833  issubassa  17973  sraassa  17974  psrbaglesupp  18017  psrbaglesuppOLD  18018  psrbaglecl  18019  psrbagcon  18022  psrgrp  18051  psrlmod  18054  psrring  18066  psrassa  18069  psgndiflemB  18636  ipdir  18674  ipdi  18675  ipsubdir  18677  ipsubdi  18678  ipass  18680  ipassr  18681  ipassr2  18682  isphld  18689  ocvlss  18703  mamudm  18890  matring  18945  matassa  18946  ofco2  18953  ma1repveval  19073  mdetunilem1  19114  mdetunilem9  19122  chpscmatgsumbin  19345  iinopn  19411  restopnb  19676  subbascn  19755  nrmsep2  19857  isnrm3  19860  regsep2  19877  dnsconst  19879  dfcon2  19920  1stcelcls  19962  dislly  19998  ptuni2  20077  tx1stc  20151  0nelfb  20332  infil  20364  fsubbas  20368  filssufilg  20412  hauspwpwf1  20488  cnextcn  20567  tmdcn2  20588  ustuqtoplem  20742  utopsnneiplem  20750  psmettri  20815  isxmet2d  20830  xmettri  20854  xmetres2  20864  bldisj  20901  blss2ps  20906  blss2  20907  xmstri2  20969  mstri2  20970  xmstri  20971  mstri  20972  xmstri3  20973  mstri3  20974  msrtri  20975  comet  21016  stdbdbl  21020  met2ndci  21025  ngprcan  21129  ngplcan  21130  ngpsubcan  21133  nrgdsdi  21174  nrgdsdir  21175  nlmdsdi  21190  nlmdsdir  21191  blcvx  21303  icoopnst  21439  pi1grplem  21549  cvsdiv  21609  cvsdivcl  21610  cphdivcl  21629  cphsubdir  21654  cphsubdi  21655  tchcph  21680  bcthlem5  21767  volfiniun  21957  volcn  22015  itg1val2  22091  dvconst  22320  dvlip  22394  ftc1a  22438  ulmval  22775  ulmdvlem3  22797  ang180  23146  cvxcl  23314  scvxcvx  23315  sgmmul  23476  dchrabl  23529  motgrp  23930  f1otrge  24175  colinearalglem1  24209  axcgrtr  24218  axeuclidlem  24265  axcontlem3  24269  axcontlem4  24270  axcontlem7  24273  eengtrkg  24288  eengtrkge  24289  isspthonpth  24586  wlkdvspth  24610  clwlkfoclwwlk  24845  el2spthonot0  24871  el2wlkonotot0  24872  usg2wotspth  24884  2spontn0vne  24887  rusgranumwlks  24956  rusgranumwwlkg  24959  iseupa  24965  3vfriswmgra  25005  frgrareggt1  25116  grpomuldivass  25251  grponpncan  25257  grpodiveq  25258  ablomuldiv  25291  ablodivdiv4  25293  ablonnncan1  25297  nvmdi  25545  nvsubadd  25550  dipassr  25761  archiabllem2c  27739  dvrdir  27780  dvrcan5  27783  reofld  27830  pstmfval  27875  qqhval2lem  27962  qqhvq  27968  measdivcstOLD  28195  measdivcst  28196  erdszelem9  28643  rescon  28691  cvmseu  28721  cvmlift2lem10  28757  cvmlift2lem12  28759  elmrsubrn  28880  mclsind  28930  frrlem4  29390  cgrid2  29653  segconeu  29661  btwncomim  29663  btwnswapid  29667  trisegint  29678  cgrxfr  29705  brofs2  29727  endofsegid  29735  btwnconn2  29752  seglemin  29763  segletr  29764  btwnsegle  29767  colinbtwnle  29768  broutsideof2  29772  btwnoutside  29775  broutsideof3  29776  outsideoftr  29779  outsidele  29782  fvray  29791  fvline  29794  ellines  29802  ftc1anc  30098  sdclem1  30236  sstotbnd2  30270  iscringd  30396  irrapxlem6  30763  jm2.26lem3  30943  dgrsub2  31084  mpaaroot  31104  mendring  31141  mendlmod  31142  mendassa  31143  rfcnpre3  31408  fmuldfeq  31577  stoweidlem43  31825  stoweidlem52  31834  stoweidlem53  31835  stoweidlem56  31838  stoweidlem57  31839  stoweidlem60  31842  ltsubsubaddltsub  32324  copissgrp  32496  initoeu2lem0  32619  initoeu2lem1  32620  cznrng  32763  funcringcsetcOLD2lem9  32852  funcringcsetclem9OLD  32875  ldepsprlem  33073  lincresunit3  33082  lincreslvec3  33083  bnj1098  33842  bnj149  33933  bnj1118  34040  lsmsat  34733  lfladdcl  34796  lflnegcl  34800  lflvscl  34802  eqlkr  34824  lshpkrlem4  34838  lshpkrlem6  34840  ldualgrplem  34870  lduallmodlem  34877  latmassOLD  34954  latm12  34955  latm32  34956  latmrot  34957  latmmdiN  34959  latmmdir  34960  omlfh1N  34983  omlfh3N  34984  cvrnbtwn2  35000  cvlexchb1  35055  cvlsupr2  35068  hlatjass  35094  hlatj12  35095  hlatj32  35096  cvrat  35146  cvrat2  35153  atltcvr  35159  atexchltN  35165  cvrat3  35166  cvrat4  35167  atbtwnexOLDN  35171  atbtwnex  35172  3dimlem3  35185  3dimlem3OLDN  35186  3at  35214  2atneat  35239  llncmp  35246  2at0mat0  35249  2atmat0  35250  llncvrlpln  35282  lplncmp  35286  2llnjaN  35290  4atlem11  35333  lplncvrlvol  35340  lvolcmp  35341  2atm2atN  35509  elpaddatriN  35527  paddasslem8  35551  paddass  35562  padd12N  35563  paddssw2  35568  paddss  35569  pmod1i  35572  pmodN  35574  pmapjlln1  35579  atmod1i1  35581  atmod1i2  35583  pexmidlem2N  35695  pl42lem2N  35704  pl42lem3N  35705  pl42lem4N  35706  pl42N  35707  lhpm0atN  35753  lautlt  35815  lautcvr  35816  lautj  35817  lautm  35818  ltrneq2  35872  cdlemd1  35923  cdleme1b  35951  cdleme1  35952  cdleme2  35953  cdleme3e  35957  cdlemefr27cl  36129  cdlemefs27cl  36139  cdleme42ke  36211  cdleme42mN  36213  cdlemf2  36288  cdlemftr2  36292  trljco  36466  tgrpgrplem  36475  tendoplass  36509  tendodi1  36510  tendodi2  36511  cdlemk34  36636  cdlemk36  36639  erngdvlem3-rN  36724  tendospdi1  36747  dialss  36773  dvhvaddass  36824  dvhopvsca  36829  dvhlveclem  36835  diblss  36897  diclss  36920  diclspsn  36921  cdlemn11pre  36937  dihmeetlem12N  37045  dihmeetlem16N  37049  dihmeetlem17N  37050  dihmeetlem18N  37051  dvh4dimN  37174  lpolconN  37214  dochpolN  37217  lclkr  37260  lclkrs  37266  lcfr  37312
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