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

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

Proof of Theorem simpl2
StepHypRef Expression
1 simp2 997 . 2
21adantr 465 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  simpll2  1036  simprl2  1042  simp1l2  1090  simp2l2  1096  simp3l2  1102  3anandirs  1331  rspc3ev  3223  brcogw  5176  weniso  6250  ofmpteq  6558  tfisi  6693  mpt2sn  6891  smogt  7057  smorndom  7058  omeulem1  7250  nnmord  7300  nnmword  7301  difsnen  7619  enfixsn  7646  mapunen  7706  ac6sfi  7784  ordiso2  7961  wemaplem2  7993  wemapso  7997  wemapso2lem  7999  en2eqpr  8406  acndom  8453  infmap2  8619  cflim2  8664  cfsmolem  8671  coftr  8674  fin23lem26  8726  isf32lem9  8762  fin1a2lem9  8809  fin1a2lem10  8810  ac6num  8880  gchdomtri  9028  canth4  9046  gchpwdom  9069  gruima  9201  grudomon  9216  prn0  9388  distrlem4pr  9425  prlem934  9432  addcan  9785  addcan2  9786  ltmul1a  10416  ledivmulOLD  10444  supmul1  10533  uzsupss  11203  xaddass  11470  xleadd1a  11474  xlesubadd  11484  xmulass  11508  xlemul2a  11510  xadddilem  11515  xadddi  11516  ixxdisj  11573  ixxun  11574  ixxlb  11580  icoshftf1o  11672  icodisj  11674  lincmb01cmp  11692  iccf1o  11693  ssfzoulel  11906  modaddmulmod  12053  ltexp2a  12217  leexp2  12220  ltexp2r  12222  exple1  12225  expnlbnd2  12297  ccatass  12605  swrdnd  12657  ccatopth  12695  swrdccatin12lem2a  12710  repswccat  12757  2cshw  12781  repsco  12805  s2f1o  12864  limsupgle  13300  limsupgre  13304  addcn2  13416  mulcn2  13418  dvdsval2  13989  dvdsadd2b  14028  dvdsmod  14043  oexpneg  14049  sadass  14121  gcdass  14183  rplpwr  14194  rppwr  14195  coprmdvds2  14244  rpmulgcd2  14246  rpexp  14261  rpdvds  14265  prmdiveq  14316  odzdvds  14322  coprimeprodsq2  14334  pythagtriplem3  14342  pythagtriplem4  14343  pcdvdsb  14392  vdwnnlem1  14513  0ram  14538  ramz2  14542  ramub1lem1  14544  mremre  15001  mrieqv2d  15036  lubss  15751  lubun  15753  clatleglb  15756  clatglbss  15757  mrelatglb  15814  isnsgrp  15915  issubmnd  15948  gsumccat  16009  frmdss2  16031  nmzsubg  16242  ghmnsgima  16290  gsmsymgreqlem1  16455  psgnunilem4  16522  odmodnn0  16564  odnncl  16569  odmod  16570  oddvds  16571  odeq  16574  odmulgid  16576  odmulgeq  16579  odbezout  16580  odf1o1  16592  odf1o2  16593  odngen  16597  gexdvdsi  16603  pgpfi1  16615  odcau  16624  subgslw  16636  fislw  16645  lsmless1x  16664  lsmless2x  16665  lsmsubm  16673  lsmmod  16693  lsmmod2  16694  efgsfo  16757  odadd1  16854  odadd2  16855  odadd  16856  lsmcomx  16862  prdscmnd  16867  gsumconst  16954  srg1zr  17180  csrgbinom  17197  ring1eq0  17238  mulgass2  17247  cntzsubr  17461  isabvd  17469  0lmhm  17686  lmhmvsca  17691  reslmhm2b  17700  pwssplit1  17705  pwssplit2  17706  pwssplit3  17707  lbspss  17728  lspsnat  17791  lidldvgen  17903  issubassa  17973  evlsval2  18189  coe1subfv  18307  coe1sclmul  18323  coe1sclmul2  18325  xrsdsreclblem  18464  cssmre  18724  obs2ss  18760  uvcresum  18824  frlmsslsp  18829  frlmsslspOLD  18830  frlmup4  18835  lindff1  18855  f1lindf  18857  lsslindf  18865  islindf4  18873  mpt2matmul  18948  mamutpos  18960  scmatscmide  19009  mavmulsolcl  19053  mulmarep1gsum2  19076  mdetdiaglem  19100  mdetdiag  19101  mdetunilem1  19114  mdetunilem3  19116  mdetunilem9  19122  maducoeval2  19142  madurid  19146  slesolinvbi  19183  cramerimplem1  19185  cramerlem1  19189  cramer  19193  cpmatel2  19214  m2cpm  19242  m2pmfzmap  19248  m2cpminvid2lem  19255  m2cpminvid2  19256  decpmatmul  19273  pmatcollpw1lem2  19276  pmatcollpw1  19277  pmatcollpw2lem  19278  pmatcollpwfi  19283  pm2mpcl  19298  mply1topmatcl  19306  mp2pm2mplem2  19308  mp2pm2mplem4  19310  mp2pm2mplem5  19311  mp2pm2mp  19312  pm2mpghmlem2  19313  pm2mpghmlem1  19314  chfacfisfcpmat  19356  topssnei  19625  cnconst2  19784  cnpresti  19789  cnprest2  19791  cnpdis  19794  cnt0  19847  cnt1  19851  cnhaus  19855  sscmp  19905  hauscmp  19907  cnconn  19923  uncon  19930  finlocfin  20021  comppfsc  20033  kgen2ss  20056  ptpjopn  20113  prdstopn  20129  ptrescn  20140  qtopss  20216  kqfvima  20231  fbssint  20339  fbasrn  20385  filuni  20386  fmss  20447  rnelfm  20454  fmufil  20460  fmco  20462  flimss2  20473  flimss1  20474  flimrest  20484  cnpflf2  20501  flfcnp  20505  supnfcls  20521  fclsss1  20523  fclsss2  20524  isfcf  20535  subgntr  20605  opnsubg  20606  cldsubg  20609  ghmcnp  20613  ustuqtop1  20744  bldisj  20901  blgt0  20902  bl2in  20903  blss2ps  20906  blss2  20907  blssps  20927  blss  20928  xmetresbl  20940  lpbl  21006  blcld  21008  stdbdmopn  21021  metcnp3  21043  metcnp  21044  metcnp2  21045  txmetcnp  21050  blval2  21078  nmoix  21236  nmoi2  21237  nmotri  21246  metdsge  21353  metdseq0  21358  iocopnst  21440  xrhmeo  21446  nmhmcn  21603  cphsqrtcl2  21633  cphsqrtcl3  21634  pjth  21854  ovoliunlem2  21914  volun  21955  mbfimaopn2  22064  iblconst  22224  limcvallem  22275  dvfval  22301  dvcnp2  22323  dvcn  22324  deg1mul3le  22517  deg1tmle  22518  dvdsq1p  22561  ig1peu  22572  ig1pdvds  22577  ply1term  22601  coeid3  22637  dgrmulc  22668  dvply1  22680  aaliou2  22736  efcvx  22844  tanord  22925  eflogeq  22986  logdivlti  23005  logccv  23044  recxpcl  23056  cxplea  23077  cxpeq  23131  ang180  23146  isosctrlem2  23153  cxp2lim  23306  amgm  23320  muval1  23407  dvdssqf  23412  mumullem2  23454  mumul  23455  bcmono  23552  lgsneg  23594  lgsdilem  23597  lgsdirprm  23604  lgsdir  23605  lgsdi  23607  lgsne0  23608  brbtwn2  24208  colinearalglem1  24209  colinearalg  24213  axcgrtr  24218  axsegconlem8  24227  axsegconlem9  24228  axsegconlem10  24229  axcontlem2  24268  axcontlem10  24276  cyclispthon  24633  wwlknext  24724  clwlkisclwwlklem0  24788  erclwwlksym  24814  eleclclwwlknlem2  24818  erclwwlkneqlen  24824  erclwwlknsym  24826  vdgrfval  24895  nbhashuvtx1  24915  usgreghash2spot  25069  extwwlkfablem2  25078  numclwwlk3lem  25108  frgraregord13  25119  gxcom  25271  gxnn0add  25276  nvmul0or  25547  ipval2lem2  25614  ipval2lem5  25620  lnoadd  25673  lnosub  25674  lnomul  25675  shless  26277  shlej1  26278  kbmul  26874  homco2  26896  kbass2  27036  eliccelico  27588  elicoelioo  27589  iocinioc2  27590  iocinif  27592  difioo  27593  xrge0adddir  27682  xrge0npcan  27684  isarchi2  27729  archiabl  27742  rhmdvdsr  27808  pstmfval  27875  fmcncfil  27913  zrhnm  27950  qqhnm  27971  nexple  28005  volfiniune  28202  dya2iocnrect  28252  probinc  28360  cndprob01  28374  signswmnd  28514  cvmsss2  28719  cvmlift2lem10  28757  binomrisefac  29164  br6  29186  funsseq  29199  frrlem4  29390  cgrtriv  29652  5segofs  29656  btwnouttr2  29672  btwnxfr  29706  lineext  29726  btwnconn1lem13  29749  brsegle2  29759  nn0prpwlem  30140  blbnd  30283  ismtyima  30299  rrndstprj2  30327  ghomdiv  30346  grpokerinj  30347  diophrw  30692  eldioph2lem1  30693  diophrex  30709  rencldnfi  30755  pellexlem2  30766  pellqrexplicit  30813  infmrgelbi  30814  pellfundglb  30821  pellfund14gap  30823  rmxycomplete  30853  congadd  30904  acongeq  30921  jm2.19  30935  jm2.23  30938  jm2.20nn  30939  jm2.27  30950  jm3.1  30962  lnmepi  31031  lmhmlnmsplit  31033  hbtlem2  31073  dgraa0p  31098  idomrootle  31152  hashgcdlem  31157  proot1hash  31160  iocunico  31178  iocinico  31179  lcmass  31218  rfcnnnub  31411  snunioo2  31544  iccintsng  31563  climsuse  31614  lptre2pt  31646  limcleqr  31650  0ellimcdiv  31655  dvnprodlem1  31743  volioc  31771  stoweidlem17  31799  stoweidlem19  31801  stoweidlem20  31802  stoweidlem22  31804  stoweidlem28  31810  stoweidlem34  31816  stoweidlem44  31826  stoweidlem60  31842  wallispilem3  31849  fourierdlem42  31931  fourierdlem48  31937  fourierdlem51  31940  fourierdlem54  31943  fourierdlem74  31963  fourierdlem77  31966  fourierdlem87  31976  fourierdlem97  31986  eluzge0nn0  32329  fzoopth  32340  rmsupp0  32961  rmsuppss  32963  lincresunit3lem3  33075  lincresunit3lem2  33081  lindssnlvec  33087  bnj517  33943  lsatfixedN  34734  lssat  34741  lshpkrlem4  34838  cvrcon3b  35002  atlen0  35035  atcvreq0  35039  atnle  35042  atlatmstc  35044  atlatle  35045  cvlcvr1  35064  hlsupr2  35111  hlrelat2  35127  cvrexchlem  35143  lnnat  35151  atcvrj2b  35156  3dimlem3  35185  3dim1  35191  1cvrjat  35199  llni  35232  llni2  35236  llnexatN  35245  2llnmat  35248  lplni  35256  2atnelpln  35268  llncvrlpln2  35281  2llnmj  35284  lplnexatN  35287  lplnexllnN  35288  2llnm3N  35293  lvoli  35299  lvoli3  35301  lvolnle3at  35306  islvol2aN  35316  4atlem4a  35323  4atlem4b  35324  4atlem11  35333  lplncvrlvol2  35339  2lplnmj  35346  islinei  35464  linepmap  35499  lnjatN  35504  lncvrat  35506  lncmp  35507  elpaddn0  35524  elpaddatriN  35527  elpaddat  35528  paddcom  35537  paddss2  35542  paddss12  35543  paddasslem4  35547  paddasslem9  35552  paddasslem10  35553  pmodl42N  35575  pmapjoin  35576  llnmod1i2  35584  polcon2bN  35644  pclfinclN  35674  poml4N  35677  poml6N  35679  osumcllem1N  35680  osumcllem2N  35681  osumcllem11N  35690  osumclN  35691  pmapojoinN  35692  pexmidlem2N  35695  pexmidlem3N  35696  pexmidlem4N  35697  pexmidlem6N  35699  pexmidlem7N  35700  pl42lem2N  35704  pl42lem3N  35705  pl42lem4N  35706  pl42N  35707  lhprelat3N  35764  4atex  35800  lauteq  35819  lautco  35821  ltrncoidN  35852  ltrneq2  35872  ltrnideq  35900  trlnle  35911  trlval3  35912  cdlemc  35922  cdlemd9  35931  cdlemd  35932  cdleme21j  36062  cdleme21  36063  cdleme29ex  36100  cdlemefr27cl  36129  cdlemefs27cl  36139  cdleme32d  36170  cdleme32f  36172  cdleme35h2  36183  cdleme40m  36193  cdleme17d3  36222  cdleme48fvg  36226  cdlemeg46fvcl  36232  cdlemeg46fgN  36260  cdleme48fgv  36264  cdleme50trn3  36279  cdlemb3  36332  cdlemg8  36357  cdlemg11a  36363  cdlemg15a  36381  cdlemg15  36382  cdlemg16  36383  cdlemg16z  36385  cdlemg17dN  36389  cdlemg24  36414  cdlemg37  36415  cdlemg29  36431  cdlemg33b  36433  cdlemg38  36441  cdlemg40  36443  trlco  36453  cdlemg44b  36458  ltrncom  36464  trljco  36466  tendococl  36498  tendoplcl  36507  tendoplcom  36508  cdlemj2  36548  tendoid0  36551  tendo1ne0  36554  cdlemk25-3  36630  cdlemk36  36639  cdlemkid4  36660  cdlemk19x  36669  cdlemk53  36683  cdlemk56  36697  cdleml5N  36706  tendospcanN  36750  cdlemm10N  36845  dihord6apre  36983  dihord  36991  dihmeetlem1N  37017  dihglblem2N  37021  dihmeetlem2N  37026  dihmeetbN  37030  dihmeetlem5  37035  dihmeetlem6  37036  dihmeetlem7N  37037  dihmeetlem10N  37043  dihmeetlem12N  37045  dihmeetlem16N  37049  dihmeetlem17N  37050  dihmeetlem18N  37051  dihmeetALTN  37054  dihlspsnssN  37059  dvh3dim2  37175  dvh3dim3N  37176  lcfrlem16  37285  mapdrvallem2  37372  mapdh8ad  37506  hgmapvvlem3  37655
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