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

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

Proof of Theorem simpl1
StepHypRef Expression
1 simp1 996 . 2
21adantr 465 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  simpll1  1035  simprl1  1041  simp1l1  1089  simp2l1  1095  simp3l1  1101  3anandirs  1331  rspc3ev  3223  brcogw  5176  cocan1  6194  weniso  6250  smogt  7057  smorndom  7058  omeulem1  7250  nnmord  7300  nnmword  7301  difsnen  7619  enfixsn  7646  mapunen  7706  ac6sfi  7784  fipreima  7846  elfiun  7910  ordiso2  7961  wemaplem2  7993  wemapso  7997  en2eqpr  8406  indcardi  8443  fodomfi2  8462  iunfictbso  8516  infmap2  8619  cofsmo  8670  cfsmolem  8671  coftr  8674  fin23lem11  8718  fincssdom  8724  fin23lem26  8726  isf32lem9  8762  ac6num  8880  gchdomtri  9028  gchpwdom  9069  winainflem  9092  tskuni  9182  gruima  9201  gruf  9210  grudomon  9216  elnpi  9387  distrlem4pr  9425  prlem934  9432  addcan  9785  addcan2  9786  ltmul1a  10416  ledivmulOLD  10444  ledivmul2OLD  10448  suprleub  10532  supmul1  10533  infmrgelb  10548  suprzcl  10967  uzsupss  11203  xleadd1a  11474  xlesubadd  11484  xmulasslem3  11507  xlemul2a  11510  xadddilem  11515  xadddi2  11518  ixxun  11574  icoshftf1o  11672  snunioc  11677  lincmb01cmp  11692  iccf1o  11693  fzofzim  11869  ltexp2a  12217  leexp2  12220  ltexp2r  12222  exple1  12225  expnlbnd2  12297  ccatass  12605  swrdswrdlem  12684  ccatopth  12695  cshco  12802  repsco  12805  s2f1o  12864  limsupgre  13304  addcn2  13416  mulcn2  13418  ntrivcvgmul  13711  dvdsadd2b  14028  dvdsmod  14043  oexpneg  14049  sadass  14121  gcdass  14183  rplpwr  14194  rppwr  14195  coprmdvds2  14244  rpmulgcd2  14246  qredeq  14247  rpexp  14261  rpdvds  14265  prmdiveq  14316  odzdvds  14322  modprmn0modprm0  14332  coprimeprodsq2  14334  pythagtriplem3  14342  pcdvdsb  14392  pcgcd1  14400  qexpz  14420  pockthg  14424  vdwnnlem1  14513  0ram  14538  ramz2  14542  lubss  15751  lubun  15753  clatleglb  15756  clatglbss  15757  mrelatglb  15814  isnsgrp  15915  issubmnd  15948  ress0g  15949  gsumccat  16009  frmdss2  16031  mulgneg  16160  mulgdirlem  16166  submmulg  16177  subgmulg  16215  nmzsubg  16242  ghmmulg  16279  gsmsymgreqlem1  16455  pmtrfb  16490  psgnunilem4  16522  odmodnn0  16564  odnncl  16569  odmod  16570  odmulgid  16576  odmulgeq  16579  odf1o1  16592  odf1o2  16593  odngen  16597  gexdvdsi  16603  pgpfi1  16615  odcau  16624  subgslw  16636  fislw  16645  lsmssv  16663  lsmless1x  16664  lsmless2x  16665  lsmsubm  16673  lsmmod  16693  lsmmod2  16694  efgred  16766  cntzcmn  16848  ghmplusg  16852  odadd1  16854  odadd2  16855  odadd  16856  lsmcomx  16862  gsumconst  16954  srg1zr  17180  ring1eq0  17238  mulgass2  17247  isabvd  17469  lssintcl  17610  0lmhm  17686  lmhmvsca  17691  reslmhm2b  17700  pwssplit1  17705  pwssplit3  17707  lspfixed  17774  lspsnat  17791  lidldvgen  17903  issubassa  17973  evlsval2  18189  psrplusgpropd  18277  coe1subfv  18307  coe1mul2  18310  xrsdsreclblem  18464  regsumsupp  18658  obselocv  18759  uvcresum  18824  frlmsslsp  18829  frlmsslspOLD  18830  frlmup4  18835  lindff1  18855  f1lindf  18857  lsslindf  18865  islindf4  18873  lbslcic  18876  mhmvlin  18899  mpt2matmul  18948  mamutpos  18960  scmatscmide  19009  mavmulsolcl  19053  marrepcl  19066  mdetdiag  19101  mdetunilem1  19114  mdetunilem3  19116  mdetunilem7  19120  mdetunilem9  19122  mdetmul  19125  slesolinvbi  19183  m2pmfzmap  19248  pmatcollpwlem  19281  pmatcollpw  19282  mp2pm2mplem4  19310  chpdmatlem3  19341  chfacfisfcpmat  19356  chfacfscmulgsum  19361  chfacfpmmulgsum  19365  chfacfpmmulgsum2  19366  cayhamlem1  19367  cpmidpmatlem2  19372  cpmadugsumlemB  19375  cpmadugsumlemC  19376  cpmadugsumlemF  19377  riinopn  19417  neiint  19605  topssnei  19625  restntr  19683  iscnp4  19764  cnconst2  19784  cnrest2  19787  cnprest2  19791  cnpdis  19794  cnt0  19847  cnt1  19851  cnhaus  19855  ordthauslem  19884  cncmp  19892  fiuncmp  19904  sscmp  19905  hauscmp  19907  cnconn  19923  uncon  19930  nlly2i  19977  llynlly  19978  nllyidm  19990  finlocfin  20021  ptrescn  20140  xkococnlem  20160  qtoptop2  20200  qtopss  20216  kqfvima  20231  r0cld  20239  ordthmeolem  20302  fbssint  20339  fmf  20446  fmss  20447  elfm  20448  rnelfmlem  20453  rnelfm  20454  fmco  20462  flimss2  20473  flimss1  20474  flimrest  20484  flftg  20497  cnpflf2  20501  cnpflf  20502  flfcnp  20505  supnfcls  20521  fclsss1  20523  fclsss2  20524  fcfnei  20536  fcfelbas  20537  cnpfcfi  20541  subgntr  20605  opnsubg  20606  cldsubg  20609  ghmcnp  20613  utop2nei  20753  neipcfilu  20799  bldisj  20901  blgt0  20902  bl2in  20903  blss2ps  20906  blss2  20907  blssps  20927  blss  20928  xmetresbl  20940  lpbl  21006  blcld  21008  stdbdbl  21020  metcnp3  21043  metcnp2  21045  txmetcnp  21050  blval2  21078  nmoix  21236  nmoeq0  21243  icoopnst  21439  iocopnst  21440  xrhmeo  21446  nmhmcn  21603  cphsqrtcl2  21633  cphsqrtcl3  21634  cfil3i  21708  caublcls  21747  bcthlem5  21767  cmetcusp1OLD  21791  cmetcusp1  21792  rrxcph  21824  pjth  21854  ovoliunlem2  21914  volun  21955  volsup2  22014  mbfimaopn2  22064  iblconst  22224  itgconst  22225  dvcnp2  22323  dvcn  22324  deg1mul3le  22517  deg1tmle  22518  dvdsq1p  22561  ig1peu  22572  ig1pdvds  22577  coeid3  22637  dgrmulc  22668  efcvx  22844  tanord  22925  logdivlti  23005  logccv  23044  recxpcl  23056  cxpeq  23131  ang180  23146  isosctrlem2  23153  cxp2lim  23306  amgm  23320  muval1  23407  dvdssqf  23412  mumullem2  23454  mumul  23455  bcmono  23552  lgsfcl2  23577  lgsdilem  23597  lgsdirprm  23604  lgsdir  23605  lgsdi  23607  lgsne0  23608  padicabv  23815  brbtwn2  24208  colinearalglem1  24209  colinearalg  24213  axcgrtr  24218  axsegconlem8  24227  axsegconlem9  24228  axsegconlem10  24229  axcontlem8  24274  axcontlem10  24276  2pthon  24604  clwwlkfo  24797  clwwlkext2edg  24802  erclwwlksym  24814  erclwwlknsym  24826  clwlkfoclwwlk  24845  clwlkf1clwwlklem  24849  numclwwlk2lem1  25102  numclwwlk5  25112  frgraregord13  25119  gxcom  25271  gxnn0add  25276  zerdivemp1  25436  nvmul0or  25547  ipval2lem2  25614  ipval2lem5  25620  lnomul  25675  shless  26277  shlej1  26278  pjspansn  26495  hoadddi  26722  kbmul  26874  homco2  26896  kbass2  27036  eliccelico  27588  elicoelioo  27589  iocinioc2  27590  iocinif  27592  xrge0adddir  27682  xrge0npcan  27684  archiabl  27742  ress1r  27779  rhmdvdsr  27808  pstmfval  27875  fmcncfil  27913  zrhnm  27950  qqhnm  27971  measvunilem  28183  volfiniune  28202  dya2iocnrect  28252  sibfinima  28281  probun  28358  probinc  28360  cndprob01  28374  pconpi1  28682  cvmsss2  28719  mrsubcv  28870  msubvrs  28920  binomrisefac  29164  dvdspw  29175  br6  29186  br4  29187  frrlem4  29390  cgrcomim  29639  cgrtriv  29652  cgrextend  29658  segconeq  29660  btwntriv2  29662  btwnintr  29669  btwnexch3  29670  btwnouttr2  29672  trisegint  29678  cgrsub  29695  cgrxfr  29705  btwnxfr  29706  lineext  29726  btwnconn1lem13  29749  btwnconn1lem14  29750  btwnconn3  29753  segcon2  29755  brsegle  29758  brsegle2  29759  segletr  29764  segleantisym  29765  seglelin  29766  outsideofeu  29781  lineunray  29797  lineelsb2  29798  areacirc  30112  ivthALT  30153  cocanfo  30208  upixp  30220  ismtyima  30299  rrndstprj2  30327  zerdivemp1x  30358  mzprename  30682  eldioph2lem1  30693  lzunuz  30701  rencldnfi  30755  pellexlem2  30766  infmrgelbi  30814  pellfundglb  30821  pellfund14gap  30823  qirropth  30844  rmxycomplete  30853  congadd  30904  acongeq  30921  jm2.19  30935  jm2.23  30938  jm2.20nn  30939  jm2.27  30950  jm3.1  30962  aomclem6  31005  lnmepi  31031  lmhmfgsplit  31032  lmhmlnmsplit  31033  pwssplit4  31035  hbtlem2  31073  hbtlem5  31077  dgraa0p  31098  hashgcdlem  31157  proot1hash  31160  iocunico  31178  lcmass  31218  suprnmpt  31451  snunioo2  31544  snunioo1  31552  iccintsng  31563  lptre2pt  31646  limcleqr  31650  volioc  31771  iblspltprt  31772  stoweidlem19  31801  stoweidlem20  31802  stoweidlem22  31804  stoweidlem28  31810  stoweidlem34  31816  stoweidlem44  31826  stoweidlem60  31842  wallispilem3  31849  fourierdlem41  31930  fourierdlem42  31931  fourierdlem49  31938  fourierdlem51  31940  fourierdlem54  31943  fourierdlem74  31963  fourierdlem97  31986  fzoopth  32340  lidldomn1  32727  ofaddmndmap  32933  lincdifsn  33025  lincellss  33027  lincresunit3lem3  33075  islindeps2  33084  lindssnlvec  33087  bnj517  33943  bnj594  33970  lsatfixedN  34734  lssat  34741  eqlkr  34824  eqlkr2  34825  lkrlsp  34827  lshpkrlem4  34838  opposet  34906  cvrcon3b  35002  cvrcmp  35008  atlen0  35035  atnle  35042  atlatmstc  35044  cvlatexch3  35063  cvlsupr2  35068  hlsupr2  35111  hlrelat2  35127  cvrexchlem  35143  lnnat  35151  atcvrj2b  35156  atle  35160  atexchcvrN  35164  atbtwn  35170  athgt  35180  3dimlem3  35185  3dim1  35191  1cvratlt  35198  1cvrjat  35199  ps-1  35201  ps-2  35202  3atlem3  35209  3atlem5  35211  3atlem7  35213  llni  35232  llni2  35236  atcvrlln2  35243  llnexatN  35245  llncmp  35246  2llnmat  35248  2at0mat0  35249  lplni  35256  lplnnle2at  35265  2atnelpln  35268  lplnllnneN  35280  llncvrlpln2  35281  2lplnmN  35283  2llnmj  35284  lplncmp  35286  lplnexatN  35287  lplnexllnN  35288  2llnm3N  35293  lvoli  35299  lvoli3  35301  islvol2aN  35316  4atlem0a  35317  4atlem3  35320  4atlem3a  35321  4atlem4a  35323  4atlem4b  35324  4atlem4c  35325  4atlem4d  35326  4atlem10b  35329  4atlem11  35333  4atlem12  35336  lplncvrlvol2  35339  lvolcmp  35341  2lplnmj  35346  islinei  35464  pmapglbx  35493  linepmap  35499  lneq2at  35502  lnjatN  35504  lncvrat  35506  lncmp  35507  2llnma3r  35512  elpaddatriN  35527  elpaddat  35528  paddcom  35537  paddss1  35541  paddss2  35542  paddss12  35543  paddasslem6  35549  paddasslem7  35550  paddasslem8  35551  paddasslem9  35552  paddasslem15  35558  pmodlem2  35571  pmodl42N  35575  pmapjoin  35576  llnmod1i2  35584  2polcon4bN  35642  polcon2bN  35644  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  lhpexle2lem  35733  lhpexle3lem  35735  lhpexle3  35736  lhpmcvr3  35749  lhp2at0nle  35759  lhprelat3N  35764  4atex  35800  4atex2  35801  lauteq  35819  lautco  35821  ltrncoidN  35852  ltrneq2  35872  ltrnnidn  35899  ltrnideq  35900  trlnid  35904  ltrnatlw  35908  trlnle  35911  trlval3  35912  trlval4  35913  cdlemc  35922  cdlemd5  35927  cdlemd9  35931  ltrneq3  35933  cdleme0moN  35950  cdleme20  36050  cdleme21j  36062  cdleme21  36063  cdleme27cl  36092  cdlemefrs29bpre0  36122  cdlemefs27cl  36139  cdlemefs32sn1aw  36140  cdleme43fsv1snlem  36146  cdleme32d  36170  cdleme32f  36172  cdleme32le  36173  cdleme35h2  36183  cdleme38n  36190  cdleme40m  36193  cdleme41snaw  36202  cdleme42ke  36211  cdleme17d3  36222  cdleme48fvg  36226  cdlemeg46fvcl  36232  cdlemeg46fgN  36260  cdleme48gfv1  36262  cdleme48fgv  36264  cdleme50trn3  36279  trlord  36295  ltrniotavalbN  36310  cdlemb3  36332  cdlemg6c  36346  cdlemg6  36349  cdlemg7N  36352  cdlemg8c  36355  cdlemg8  36357  cdlemg11a  36363  cdlemg11b  36368  cdlemg12e  36373  cdlemg15a  36381  cdlemg15  36382  cdlemg16  36383  cdlemg16z  36385  cdlemg16zz  36386  cdlemg17dN  36389  cdlemg18a  36404  cdlemg20  36411  cdlemg22  36413  cdlemg24  36414  cdlemg37  36415  cdlemg31d  36426  cdlemg29  36431  cdlemg33b  36433  cdlemg33  36437  cdlemg38  36441  cdlemg39  36442  cdlemg40  36443  trlco  36453  trlcone  36454  cdlemg42  36455  cdlemg44b  36458  ltrncom  36464  trljco  36466  tendococl  36498  tendoplcl  36507  tendoplcom  36508  cdlemj2  36548  cdlemj3  36549  tendoid0  36551  tendoconid  36555  tendotr  36556  cdlemk25-3  36630  cdlemk26b-3  36631  cdlemk34  36636  cdlemk36  36639  cdlemk38  36641  cdlemkid4  36660  cdlemk35s-id  36664  cdlemk39s-id  36666  cdlemk19x  36669  cdlemk53  36683  cdlemk55  36687  cdlemk55u  36692  cdlemk39u  36694  cdlemk19u  36696  cdlemk56  36697  tendoex  36701  cdleml3N  36704  cdleml5N  36706  tendospcanN  36750  cdlemm10N  36845  cdlemn11pre  36937  dihord2pre  36952  dihvalcqpre  36962  dihopelvalcpre  36975  dihord6apre  36983  dihord5b  36986  dihord5apre  36989  dihord  36991  dihmeetlem1N  37017  dihglblem5apreN  37018  dihglblem3N  37022  dihmeetlem2N  37026  dihglbcpreN  37027  dihmeetbN  37030  dihmeetlem4preN  37033  dihmeetlem5  37035  dihmeetlem7N  37037  dihmeetlem10N  37043  dihmeetlem11N  37044  dihmeetlem12N  37045  dihmeetlem13N  37046  dihmeetlem15N  37048  dihmeetlem16N  37049  dihmeetlem17N  37050  dihmeetlem18N  37051  dihmeetlem19N  37052  dihmeetALTN  37054  dih1dimatlem0  37055  dihlspsnssN  37059  dihlspsnat  37060  mapdh8ad  37506  hdmap14lem14  37611  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