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

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

Proof of Theorem simpl3
StepHypRef Expression
1 simp3 998 . 2
21adantr 465 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  simpll3  1037  simprl3  1043  simp1l3  1091  simp2l3  1097  simp3l3  1103  3anandirs  1331  fcofo  6191  soisores  6223  weniso  6250  knatar  6253  ofmpteq  6558  smorndom  7058  nnmord  7300  nnmword  7301  difsnen  7619  mapunen  7706  ac6sfi  7784  fipreima  7846  wemaplem2  7993  wemapso2lem  7999  en2eqpr  8406  indcardi  8443  acndom  8453  fodomfi2  8462  infmap2  8619  cflim2  8664  coftr  8674  infpssrlem4  8707  fin23lem11  8718  fincssdom  8724  isf32lem9  8762  fin1a2lem9  8809  gchpwdom  9069  gruima  9201  prpssnq  9389  distrlem4pr  9425  dedekind  9765  addcan  9785  addcan2  9786  ledivmul2OLD  10448  supmul1  10533  uzsupss  11203  xaddass  11470  xleadd1a  11474  xlesubadd  11484  xmulasslem3  11507  xmulass  11508  xadddilem  11515  xadddi  11516  ixxun  11574  icoshftf1o  11672  snunioc  11677  difelfzle  11817  fzo1fzo0n0  11864  ssfzoulel  11906  modifeq2int  12049  modaddmulmod  12053  modsubdir  12055  ltexp2a  12217  leexp2  12220  ltexp2r  12222  exple1  12225  expnlbnd2  12297  hashtpg  12523  ccatass  12605  swrdnd  12657  ccatopth  12695  swrdccatin12lem2a  12710  swrdccat3  12717  s2f1o  12864  limsuplt  13302  limsupgre  13304  addcn2  13416  mulcn2  13418  dvdsmod  14043  sadass  14121  gcdass  14183  rplpwr  14194  rppwr  14195  rpmulgcd2  14246  rpexp  14261  rpdvds  14265  prmdiveq  14316  coprimeprodsq  14333  coprimeprodsq2  14334  pythagtriplem3  14342  pcdvdsb  14392  pcgcd1  14400  pcbc  14419  0ram  14538  ramz2  14542  ramub1lem1  14544  mremre  15001  mrieqv2d  15036  lubun  15753  isnsgrp  15915  issubmnd  15948  gsumccat  16009  frmdss2  16031  sgrp2rid2ex  16045  mulgnn0p1  16153  mulgnnsubcl  16154  mulgneg  16160  mulgdirlem  16166  nmzsubg  16242  ghmmulg  16279  pmtrfv  16477  pmtrmvd  16481  pmtrfb  16490  odmodnn0  16564  oddvdsnn0  16568  odnncl  16569  odmod  16570  oddvds  16571  odeq  16574  odmulgid  16576  odmulg  16578  odmulgeq  16579  odbezout  16580  odf1o1  16592  odf1o2  16593  odngen  16597  odcau  16624  pgpssslw  16634  fislw  16645  lsmless1x  16664  lsmless2x  16665  lsmsubm  16673  lsmmod  16693  lsmmod2  16694  efgsfo  16757  cntzcmn  16848  odadd1  16854  odadd2  16855  odadd  16856  lsmcomx  16862  prdscmnd  16867  gsumconst  16954  ring1eq0  17238  cntzsubr  17461  isabvd  17469  lspss  17630  0lmhm  17686  reslmhm2  17699  pwssplit0  17704  pwssplit1  17705  lbspss  17728  lspfixed  17774  lsmcv  17787  lspsnat  17791  issubassa  17973  aspss  17981  coe1subfv  18307  coe1tm  18314  xrsdsreclblem  18464  obselocv  18759  frlmsplit2  18803  frlmsslss2  18805  frlmsslss2OLD  18806  frlmup4  18835  lindff1  18855  lsslindf  18865  lsslinds  18866  islindf4  18873  mpt2matmul  18948  mamutpos  18960  submaval  19083  mdetdiag  19101  mdetunilem1  19114  mdetunilem3  19116  mdetunilem9  19122  mdetmul  19125  maducoeval2  19142  madurid  19146  minmar1val  19150  cramer  19193  cpmatel2  19214  m2cpm  19242  decpmatmul  19273  pmatcollpw1lem2  19276  pmatcollpw1  19277  pmatcollpw2lem  19278  pm2mpcl  19298  mply1topmatcl  19306  mp2pm2mplem2  19308  mp2pm2mplem4  19310  pm2mpghmlem2  19313  pm2mpghmlem1  19314  cayhamlem2  19385  neiint  19605  topssnei  19625  cnrest2  19787  cnprest2  19791  cnt0  19847  cnt1  19851  cnhaus  19855  cncmp  19892  fiuncmp  19904  sscmp  19905  hauscmp  19907  cnconn  19923  uncon  19930  comppfsc  20033  kgen2ss  20056  ptpjopn  20113  ptrescn  20140  qtopss  20216  kqfvima  20231  r0cld  20239  cmphaushmeo  20301  fbssint  20339  fbasrn  20385  filuni  20386  ufilmax  20408  fin1aufil  20433  fmf  20446  fmss  20447  rnelfmlem  20453  rnelfm  20454  fmufil  20460  fmco  20462  flimss2  20473  flimss1  20474  flimrest  20484  cnpflf2  20501  cnpflf  20502  flfcnp  20505  lmflf  20506  supnfcls  20521  fclsss1  20523  fclsss2  20524  cnpfcfi  20541  subgntr  20605  opnsubg  20606  cldsubg  20609  ustuqtop1  20744  ucncn  20788  bldisj  20901  blgt0  20902  bl2in  20903  blss2ps  20906  blss2  20907  xbln0  20917  blssps  20927  blss  20928  lpbl  21006  blcld  21008  blcls  21009  stdbdmopn  21021  metcnp2  21045  txmetcnp  21050  blval2  21078  restmetu  21090  nmoix  21236  nmoi2  21237  nmoeq0  21243  nmotri  21246  metdsge  21353  metds0  21354  metdseq0  21358  icoopnst  21439  iccpnfhmeo  21445  xrhmeo  21446  nmhmcn  21603  cphsqrtcl2  21633  cphsqrtcl3  21634  fmcfil  21711  bcthlem5  21767  cmetcusp1OLD  21791  cmetcusp1  21792  pjth  21854  ovolunnul  21911  volun  21955  voliunlem2  21961  itg2const  22147  iblconst  22224  itgconst  22225  limcvallem  22275  dvcnp2  22323  dvcn  22324  deg1mul3le  22517  deg1tmle  22518  ig1pdvds  22577  coe11  22650  dgrmulc  22668  dvply1  22680  aaliou2  22736  efcvx  22844  tanord  22925  logdivlti  23005  logccv  23044  recxpcl  23056  cxplea  23077  cxple2a  23080  ang180  23146  isosctrlem2  23153  cxp2lim  23306  amgm  23320  muval1  23407  dvdssqf  23412  mumullem2  23454  bcmono  23552  lgsneg  23594  lgsmod  23596  lgsdirprm  23604  lgsdir  23605  lgsdi  23607  brbtwn2  24208  colinearalglem1  24209  colinearalg  24213  axcgrtr  24218  axcontlem2  24268  cyclispthon  24633  clwwlknprop  24772  clwwlknimp  24776  vdgrfif  24899  4cyclusnfrgra  25019  zerdivemp1  25436  nvmul0or  25547  shless  26277  shlej1  26278  pjspansn  26495  kbmul  26874  homco2  26896  kbass2  27036  eliccelico  27588  elicoelioo  27589  iocinioc2  27590  difioo  27593  xrge0npcan  27684  isarchi2  27729  archiabl  27742  pstmfval  27875  fmcncfil  27913  zrhnm  27950  qqhnm  27971  nexple  28005  volfiniune  28202  eulerpartlemb  28307  probinc  28360  cndprob01  28374  signswmnd  28514  cvmsss2  28719  binomrisefac  29164  dvdspw  29175  funsseq  29199  sltres  29424  cgrtriv  29652  5segofs  29656  btwntriv2  29662  btwnxfr  29706  segcon2  29755  brsegle2  29759  seglelin  29766  outsideofeu  29781  bpolydif  29817  mblfinlem2  30052  blbnd  30283  rrndstprj2  30327  zerdivemp1x  30358  mzpsubst  30681  diophrw  30692  eldioph2lem1  30693  rencldnfi  30755  pellexlem2  30766  pellqrexplicit  30813  infmrgelbi  30814  rmxycomplete  30853  congadd  30904  acongeq  30921  jm2.19  30935  jm2.22  30937  jm2.20nn  30939  jm2.25lem1  30940  jm2.27  30950  jm3.1  30962  lmhmlnmsplit  31033  pwssplit4  31035  hbtlem2  31073  dgraa0p  31098  idomrootle  31152  hashgcdlem  31157  proot1hash  31160  iocunico  31178  lcmass  31218  suprnmpt  31451  snunioo1  31552  iccintsng  31563  fmul01  31574  lptre2pt  31646  0ellimcdiv  31655  ibliccsinexp  31749  iblioosinexp  31751  volioc  31771  iblspltprt  31772  stoweidlem20  31802  stoweidlem22  31804  stoweidlem34  31816  stoweidlem44  31826  stoweidlem60  31842  wallispilem3  31849  fourierdlem42  31931  fourierdlem51  31940  fourierdlem54  31943  fourierdlem87  31976  fourierdlem97  31986  lincresunit3lem3  33075  lindssnlvec  33087  lsmsat  34733  lsatfixedN  34734  lssat  34741  lkrlsp  34827  lshpkrlem4  34838  cvrcon3b  35002  leat3  35020  atlen0  35035  atnle  35042  atlatmstc  35044  atlatle  35045  cvlcvr1  35064  cvlsupr2  35068  hlsupr2  35111  hlrelat2  35127  cvrexchlem  35143  cvratlem  35145  lnnat  35151  atexchcvrN  35164  1cvratlt  35198  1cvrjat  35199  3atlem3  35209  3atlem7  35213  llni2  35236  atcvrlln2  35243  llnexatN  35245  llncmp  35246  2llnmat  35248  2at0mat0  35249  2atnelpln  35268  llncvrlpln2  35281  2lplnmN  35283  2llnmj  35284  lplncmp  35286  lplnexatN  35287  2llnjaN  35290  lvoli3  35301  islvol2aN  35316  4atlem3a  35321  4atlem4a  35323  4atlem4b  35324  4atlem11  35333  4atlem12  35336  lplncvrlvol2  35339  lvolcmp  35341  2lplnmj  35346  islinei  35464  linepmap  35499  lneq2at  35502  2llnma3r  35512  elpaddn0  35524  elpaddatriN  35527  elpaddat  35528  paddcom  35537  paddss1  35541  paddss2  35542  paddasslem6  35549  paddasslem7  35550  paddasslem10  35553  paddasslem15  35558  pmodlem2  35571  pmodl42N  35575  pmapjoin  35576  atmod1i1m  35582  llnmod1i2  35584  llnexchb2lem  35592  polcon2bN  35644  pclfinclN  35674  poml4N  35677  poml6N  35679  osumcllem11N  35690  osumclN  35691  pmapojoinN  35692  pexmidlem2N  35695  pexmidlem3N  35696  pexmidlem4N  35697  pexmidlem6N  35699  pexmidlem7N  35700  pl42lem2N  35704  pl42lem3N  35705  pl42lem4N  35706  pl42N  35707  lhpexle3lem  35735  lhpmcvr3  35749  lhp2at0nle  35759  lhprelat3N  35764  lauteq  35819  lautco  35821  ltrncoidN  35852  ltrneq2  35872  ltrnnidn  35899  ltrnideq  35900  trlnle  35911  cdlemc  35922  cdlemd4  35926  cdlemd5  35927  cdlemd9  35931  cdlemd  35932  ltrneq3  35933  cdlemefrs29pre00  36121  cdlemefrs29cpre1  36124  cdlemefrs29clN  36125  cdlemefrs32fva  36126  cdlemefr29exN  36128  cdlemefr27cl  36129  cdlemefs27cl  36139  cdlemefs32sn1aw  36140  cdleme32fva  36163  cdleme32d  36170  cdleme32f  36172  cdleme32le  36173  cdleme40n  36194  cdleme41snaw  36202  cdleme17d3  36222  cdleme48fvg  36226  cdlemeg46fvcl  36232  cdlemeg46fgN  36260  cdleme48fgv  36264  ltrniotavalbN  36310  cdlemb3  36332  cdlemg15  36382  cdlemg17dN  36389  trlco  36453  cdlemg44b  36458  ltrncom  36464  trljco  36466  tendococl  36498  tendoplcl  36507  tendoplcom  36508  tendotr  36556  cdlemk36  36639  cdlemk35s-id  36664  cdlemk39s-id  36666  cdlemk19x  36669  cdlemk53b  36682  cdlemk55  36687  cdlemk35u  36690  cdlemk55u  36692  cdlemk39u  36694  cdlemk19u  36696  cdlemk56  36697  tendoex  36701  cdleml5N  36706  dihord2pre  36952  dihord6apre  36983  dihord5b  36986  dihord5apre  36989  dihord  36991  dihmeetlem1N  37017  dihmeetlem2N  37026  dihglbcpreN  37027  dihmeetbN  37030  dihmeetlem4preN  37033  dihmeetlem5  37035  dihmeetlem6  37036  dihmeetlem7N  37037  dihmeetlem10N  37043  dihmeetlem11N  37044  dihmeetlem12N  37045  dihmeetlem13N  37046  dihmeetlem15N  37048  dihmeetlem17N  37050  dihmeetlem18N  37051  dihmeetlem19N  37052  dihmeetALTN  37054  dih1dimatlem0  37055  dihlspsnssN  37059  dvh3dim2  37175
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