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

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

Proof of Theorem simpr3
StepHypRef Expression
1 simp3 998 . 2
21adantl 466 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  simplr3  1040  simprr3  1046  simp1r3  1094  simp2r3  1100  simp3r3  1106  3anandis  1330  isopolem  6241  fr3nr  6615  suppfnss  6944  elfir  7895  intrnfi  7896  fisupcl  7948  cnfcomlem  8164  cnfcomlemOLD  8172  ackbij1lem15  8635  pwfseqlem4a  9060  pwfseqlem4  9061  eluzuzle  11118  xlesubadd  11484  elioc2  11616  elico2  11617  elicc2  11618  fseq1p1m1  11781  swrdsymbeq  12672  ccatswrd  12681  modfsummods  13607  tanadd  13902  dvds2ln  14014  cshwsidrepsw  14578  ressress  14694  f1ovscpbl  14923  mreexexlem4d  15044  mreexexd  15045  2oppccomf  15120  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  imasmnd2  15957  imasmnd  15958  frmdmnd  16027  grpsubadd  16126  grpaddsubass  16128  grpsubsub4  16131  grppnpcan2  16132  grpnpncan  16133  grpnnncan2  16135  mulgnndir  16164  mulgnn0dir  16165  mulgnnass  16170  mulgnn0ass  16171  mulgass  16172  pwsmulg  16184  imasgrp2  16185  imasgrp  16186  issubg2  16216  qusgrp  16256  galcan  16342  gacan  16343  oppgmnd  16389  symggrp  16425  pmtrprfv  16478  pmtr3ncom  16500  psgnunilem3  16521  frgp0  16778  cmn32  16816  cmn12  16818  abladdsub  16825  mulgdi  16835  mulgsubdi  16838  dprdss  17076  dprdf1o  17079  dprdsn  17083  dmdprdsplit  17096  pgpfac1lem5  17130  srgi  17163  ringi  17211  prdsringd  17261  imasring  17268  opprring  17280  mulgass3  17286  dvrass  17339  kerf1hrm  17392  subrgunit  17447  issubrg2  17449  abvdiv  17486  lss1  17585  lsssn0  17594  islss3  17605  prdslmodd  17615  islmhm2  17684  lspsolv  17789  lbsextlem4  17807  sralmod  17833  issubassa  17973  sraassa  17974  psrbaglesupp  18017  psrbaglesuppOLD  18018  psrbagcon  18022  psrgrp  18051  psrlmod  18054  psrring  18066  psrassa  18069  mpllsslem  18094  mpllsslemOLD  18096  ipdi  18675  ipsubdir  18677  ipsubdi  18678  ipassr  18681  ipassr2  18682  isphld  18689  ocvlss  18703  mamudm  18890  matring  18945  matassa  18946  ofco2  18953  scmatlss  19027  ma1repveval  19073  mdetunilem1  19114  mdetunilem9  19122  monmatcollpw  19280  iinopn  19411  restopnb  19676  subbascn  19755  nrmsep2  19857  isnrm3  19860  t1sep  19871  regsep2  19877  dnsconst  19879  dfcon2  19920  dislly  19998  tx1stc  20151  qtophmeo  20318  filss  20354  infil  20364  fsubbas  20368  filssufilg  20412  hauspwpwf1  20488  cnextcn  20567  tmdcn2  20588  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  met2ndci  21025  ngprcan  21129  ngplcan  21130  ngpsubcan  21133  nrgdsdi  21174  nrgdsdir  21175  nlmdsdi  21190  nlmdsdir  21191  blcvx  21303  iocopnst  21440  icccvx  21450  pi1grplem  21549  pi1xfrf  21553  pi1cof  21559  cvsdiv  21609  cvsdivcl  21610  cphdivcl  21629  cphsubdir  21654  cphsubdi  21655  bcthlem5  21767  rrxcph  21824  volfiniun  21957  volcn  22015  itg1val2  22091  dvconst  22320  dvlip  22394  ftc1a  22438  ulmdvlem3  22797  ang180  23146  cvxcl  23314  scvxcvx  23315  sgmmul  23476  logexprlim  23500  dchrabl  23529  motgrp  23930  f1otrge  24175  xmstrkgc  24189  colinearalglem1  24209  colinearalg  24213  axcgrtr  24218  axlowdimlem16  24260  axeuclidlem  24265  axcontlem4  24270  axcontlem7  24273  axcontlem12  24278  eengtrkg  24288  eengtrkge  24289  isspthonpth  24586  wlkdvspth  24610  usg2wotspth  24884  2pthwlkonot  24885  rusgranumwwlkg  24959  numclwwlk5  25112  friendship  25122  grpomuldivass  25251  grpopnpcan2  25255  grponpncan  25257  grpodiveq  25258  ablodivdiv4  25293  ablonnncan  25295  ismndo1  25346  nvsubadd  25550  dipdi  25758  dipsubdi  25764  disjdsct  27521  omndmul2  27702  archiabllem2c  27739  dvrdir  27780  dvrcan5  27783  reofld  27830  pstmfval  27875  qqhval2lem  27962  qqhvq  27968  esumcvg  28092  sigaclcu  28117  measdivcstOLD  28195  measdivcst  28196  erdszelem9  28643  cvmseu  28721  elmrsubrn  28880  cgrid2  29653  btwncomim  29663  btwnswapid  29667  trisegint  29678  cgrxfr  29705  btwnxfr  29706  brofs2  29727  brifs2  29728  endofsegid  29735  btwnconn1lem11  29747  btwnconn2  29752  segcon2  29755  seglemin  29763  segletr  29764  btwnsegle  29767  colinbtwnle  29768  broutsideof2  29772  btwnoutside  29775  broutsideof3  29776  outsideoftr  29779  outsidele  29782  ellines  29802  linethrueu  29806  ftc1anc  30098  sdclem1  30236  sstotbnd2  30270  zerdivemp1x  30358  isdrngo2  30361  iscringd  30396  irrapxlem6  30763  jm2.26lem3  30943  mpaamn  31105  mendring  31141  mendlmod  31142  mendassa  31143  rfcnpre4  31409  fmuldfeq  31577  stoweidlem43  31825  stoweidlem52  31834  stoweidlem53  31835  stoweidlem56  31838  copissgrp  32496  initoeu2lem1  32620  ringrng  32685  cznrng  32763  funcringcsetcOLD2lem9  32852  funcringcsetclem9OLD  32875  linccl  33015  lincsumscmcl  33034  ldepsprlem  33073  lincresunit3lem1  33080  bnj970  34005  bnj910  34006  lsmsat  34733  lfladdcl  34796  lflnegcl  34800  lflvscl  34802  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  cvlexch3  35057  cvlexch4N  35058  cvlatexchb1  35059  cvlsupr2  35068  hlatjass  35094  hlatj12  35095  hlatj32  35096  cvrat  35146  atcvrj0  35152  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  islpln2a  35272  llncvrlpln  35282  lplncmp  35286  3atnelvolN  35310  4atlem11  35333  lplncvrlvol  35340  lvolcmp  35341  2atm2atN  35509  elpaddatriN  35527  elpadd2at2  35531  paddasslem8  35551  paddasslem17  35560  paddass  35562  padd12N  35563  paddssw1  35567  pmodlem2  35571  pmodN  35574  pmapjlln1  35579  atmod1i2  35583  pexmidlem2N  35695  pexmidlem7N  35700  pl42lem2N  35704  pl42lem3N  35705  pl42lem4N  35706  pl42N  35707  lhp2lt  35725  lhpm0atN  35753  lautlt  35815  lautcvr  35816  lautj  35817  lautm  35818  ltrneq2  35872  cdleme1b  35951  cdleme3b  35954  cdleme3c  35955  cdleme9b  35977  cdlemefs27cl  36139  cdleme42mN  36213  cdlemg4c  36338  trljco  36466  tgrpgrplem  36475  tendoplass  36509  tendodi1  36510  tendodi2  36511  erngplus2  36530  erngplus2-rN  36538  cdlemk36  36639  erngdvlem3  36716  erngdvlem3-rN  36724  dvaplusgv  36736  tendospass  36746  tendospdi1  36747  dvalveclem  36752  dialss  36773  dvhvaddass  36824  dvhopvsca  36829  dvhlveclem  36835  diblss  36897  diclss  36920  diclspsn  36921  cdlemn11pre  36937  dihmeetlem12N  37045  dihmeetlem16N  37049  dihmeetlem17N  37050  dvh4dimN  37174  lpolsatN  37215  lpolpolsatN  37216  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