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

Theorem simpr1 987
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
Assertion
Ref Expression
simpr1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ps )

Proof of Theorem simpr1
StepHypRef Expression
1 simp1 981 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
21adantl 463 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 958
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 960
This theorem is referenced by:  simplr1  1023  simprr1  1029  simp1r1  1077  simp2r1  1083  simp3r1  1089  3anandis  1313  isopolem  6023  fr3nr  6380  suppfnss  6703  frfi  7545  intrnfi  7654  iinfi  7655  eqsup  7694  fisupcl  7705  cnfcomlem  7920  cnfcomlemOLD  7928  ackbij1lem15  8391  fpwwe2lem5  8788  dedekindle  9521  ico0  11333  elioc2  11345  elico2  11346  elicc2  11347  iccsplit  11404  elfzelfzelfz  11470  fseq1p1m1  11517  hashtpg  12169  swrdsymbeq  12324  ccatswrd  12333  tanadd  13433  dvds2ln  13545  qredeq  13774  ressress  14217  mreexexlem4d  14567  mreexexd  14568  0catg  14607  2oppccomf  14646  issubc3  14741  fthmon  14819  fuccocl  14856  fucidcl  14857  invfuc  14866  curf2cl  15023  yonedalem4c  15069  yonedalem3  15072  pospo  15125  latjle12  15214  latjlej1  15217  latnlej2  15223  latlem12  15230  latmlem1  15233  latledi  15241  latmlej11  15242  latjass  15247  latj12  15248  latj32  15249  latj13  15250  latj31  15251  latjrot  15252  latjjdi  15255  latjjdir  15256  latdisdlem  15341  prdsmndd  15436  imasmnd2  15440  frmdmnd  15516  grpsubrcan  15586  grpsubadd  15592  grpsubsub  15593  grpaddsubass  15594  grpsubsub4  15597  grpnnncan2  15600  mulgnndir  15628  mulgnn0dir  15629  mulgdir  15631  mulgnnass  15634  mulgnn0ass  15635  mulgass  15636  mulgsubdir  15637  pwsmulg  15648  imasgrp2  15649  issubg2  15675  eqgval  15709  divsgrp  15715  galcan  15801  gacan  15802  oppgmnd  15848  symggrp  15884  pmtrprfv  15938  pmtr3ncom  15960  psgnunilem3  15981  cmn32  16274  cmn12  16276  abladdsub  16283  mulgnn0di  16292  mulgdi  16293  mulgsubdi  16296  dprdss  16499  dprdz  16500  dprdf1o  16502  dprdsn  16506  dprd2da  16514  ablfac1b  16544  pgpfac1lem5  16553  rngi  16592  prdsrngd  16638  imasrng  16645  opprrng  16656  mulgass3  16662  dvrass  16715  subrgunit  16806  issubrg2  16808  abvdiv  16845  islss3  16961  prdslmodd  16971  islmhm2  17040  lspsolv  17145  islbs2  17156  islbs3  17157  lbsextlem4  17163  sralmod  17189  issubassa  17316  sraassa  17317  psrbaglecl  17370  psrbagcon  17373  psrgrp  17402  psrlmod  17405  psrrng  17416  psrassa  17419  ipdir  17909  ipdi  17910  ipsubdir  17912  ipsubdi  17913  ipass  17915  ipassr  17916  ipassr2  17917  ocvlss  17938  mamudm  18129  matrng  18171  matassa  18172  ofco2  18173  mdetunilem1  18259  mdetunilem9  18267  mdetuni0  18268  mdetmul  18270  gsummatr01lem3  18304  iinopn  18356  subbascn  18699  nrmsep2  18801  isnrm3  18804  regsep2  18821  dnsconst  18823  dfcon2  18864  1stcelcls  18906  nllyidm  18934  dislly  18942  upxp  19037  fbasne0  19244  filss  19267  infil  19277  fsubbas  19281  filssufilg  19325  tmdcn2  19501  psmettri  19728  isxmet2d  19743  xmettri  19767  xmetres2  19777  bldisj  19814  blss2ps  19819  blss2  19820  xmstri2  19882  mstri2  19883  xmstri  19884  mstri  19885  xmstri3  19886  mstri3  19887  msrtri  19888  comet  19929  stdbdbl  19933  met2ndci  19938  ngprcan  20042  ngplcan  20043  ngpsubcan  20046  nrgdsdi  20087  nrgdsdir  20088  nlmdsdi  20103  nlmdsdir  20104  blcvx  20216  icccmplem2  20241  pi1grplem  20462  pi1cof  20472  cvsdiv  20522  cvsdivcl  20523  cphdivcl  20542  cphsubdir  20567  cphsubdi  20568  cphassr  20571  bcthlem5  20680  rrxcph  20737  volfiniun  20869  volcn  20927  itg1val2  21003  dvconst  21232  dvlip  21306  dvfsumlem4  21342  ftc1a  21350  ulmval  21729  ulmdvlem3  21751  ang180  22094  cvxcl  22262  scvxcvx  22263  sgmmul  22424  logexprlim  22448  dchrabl  22477  f1otrge  22940  xmstrkgc  22954  colinearalglem1  22974  colinearalg  22978  axcgrtr  22983  axlowdimlem16  23025  axeuclidlem  23030  axcontlem7  23038  eengtrkg  23053  eengtrkge  23054  wlkoniswlk  23254  constr2trl  23320  wlkdvspth  23329  iseupa  23408  grpodivdiv  23557  grpomuldivass  23558  grpopnpcan2  23562  ablodivdiv4  23600  ablonnncan  23602  ablonnncan1  23604  zerdivemp1  23743  nvmdi  23852  dipassr  24068  archiabllem2c  26035  srgi  26046  dvrdir  26110  dvrcan5  26113  kerf1hrm  26144  reofld  26161  pstmfval  26176  tpr2rico  26195  qqhval2lem  26263  qqhvq  26269  issiga  26407  measdivcstOLD  26491  measdivcst  26492  signsply0  26799  erdszelem9  26934  rescon  26982  cvmseu  27012  cvmlift2lem12  27050  cgrid2  27880  segconeu  27888  btwncomim  27890  btwnswapid  27894  cgrxfr  27932  btwnxfr  27933  colineardim1  27938  brofs2  27954  brifs2  27955  idinside  27961  endofsegid  27962  btwnconn1lem7  27970  btwnconn1lem11  27974  btwnconn1  27978  segcon2  27982  seglemin  27990  segletr  27991  btwnsegle  27994  colinbtwnle  27995  broutsideof2  27999  broutsideof3  28003  outsidele  28009  fvray  28018  fvline  28021  linerflx1  28026  ellines  28029  ftc1anc  28316  ivthALT  28371  sdclem1  28480  sstotbnd2  28514  zerdivemp1x  28602  isdrngo2  28605  iscringd  28640  irrapxlem6  29010  jm2.26lem3  29192  dgrsub2  29333  mpaadgr  29353  mendrng  29391  mendlmod  29392  mendassa  29393  fmuldfeq  29606  stoweidlem43  29681  stoweidlem52  29690  stoweidlem53  29691  stoweidlem56  29694  stoweidlem57  29695  el2spthonot0  30233  el2wlkonotot0  30234  usg2wotspth  30246  2pthwlkonot  30247  erclwwlktr  30328  erclwwlkntr  30344  numclwwlk5  30548  friendship  30558  linccl  30654  lincext1  30694  lincext3  30696  lincresunit2  30718  bnj149  31567  bnj1118  31674  bnj1128  31680  lsmsat  32223  lfladdcl  32286  lflnegcl  32290  lflvscl  32292  lshpkrlem4  32328  lshpkrlem6  32330  ldualgrplem  32360  lduallmodlem  32367  latmassOLD  32444  latm12  32445  latm32  32446  latmrot  32447  latmmdiN  32449  latmmdir  32450  omlfh1N  32473  omlfh3N  32474  cvlexchb1  32545  cvlexch3  32547  cvlexch4N  32548  cvlatexchb1  32549  cvlsupr2  32558  hlatjass  32584  hlatj12  32585  hlatj32  32586  cvratlem  32635  cvrat  32636  atcvrj0  32642  cvrat2  32643  atltcvr  32649  atexchltN  32655  cvrat3  32656  cvrat4  32657  3dimlem3  32675  3dimlem3OLDN  32676  3at  32704  2atneat  32729  llncmp  32736  2at0mat0  32739  2atmat0  32740  lplnnle2at  32755  llncvrlpln  32772  lplncmp  32776  lplnexllnN  32778  2llnjaN  32780  4atlem11  32823  lplncvrlvol  32830  lvolcmp  32831  2atm2atN  32999  elpaddatriN  33017  paddasslem9  33042  paddass  33052  padd12N  33053  paddssw2  33058  paddss  33059  pmodlem2  33061  pmodN  33064  pmapjlln1  33069  atmod1i1  33071  atmod1i2  33073  pexmidlem2N  33185  pexmidlem6N  33189  pl42N  33197  lhpm0atN  33243  lautlt  33305  lautcvr  33306  lautj  33307  lautm  33308  ltrneq2  33362  cdlemc3  33407  cdlemc4  33408  cdlemd1  33412  cdleme1b  33440  cdleme1  33441  cdleme2  33442  cdleme3e  33446  cdlemefr27cl  33617  cdlemefs27cl  33627  cdleme42mN  33701  cdlemftr2  33780  trljco  33954  tgrpgrplem  33963  tendoplass  33997  tendodi1  33998  tendodi2  33999  cdlemk36  34127  erngdvlem3  34204  erngdvlem3-rN  34212  tendospdi1  34235  dvalveclem  34240  dialss  34261  dvhvaddass  34312  dvhopvsca  34317  dvhlveclem  34323  diblss  34385  diclss  34408  dihmeetlem12N  34533  dihmeetlem15N  34536  dihmeetlem16N  34537  dihmeetlem17N  34538  dihmeetlem18N  34539  dihmeetlem19N  34540  dvh4dimN  34662  lpolvN  34701  lclkr  34748  lclkrs  34754  lcfr  34800
  Copyright terms: Public domain W3C validator