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

Theorem simpr1 994
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 988 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
21adantl 466 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  simplr1  1030  simprr1  1036  simp1r1  1084  simp2r1  1090  simp3r1  1096  3anandis  1321  isopolem  6135  fr3nr  6491  suppfnss  6814  frfi  7658  intrnfi  7767  iinfi  7768  eqsup  7807  fisupcl  7818  cnfcomlem  8033  cnfcomlemOLD  8041  ackbij1lem15  8504  fpwwe2lem5  8902  dedekindle  9635  ico0  11447  elioc2  11459  elico2  11460  elicc2  11461  iccsplit  11519  elfzelfzelfz  11585  fseq1p1m1  11635  hashtpg  12288  swrdsymbeq  12443  ccatswrd  12452  tanadd  13553  dvds2ln  13665  qredeq  13894  ressress  14337  mreexexlem4d  14687  mreexexd  14688  0catg  14727  2oppccomf  14766  issubc3  14861  fthmon  14939  fuccocl  14976  fucidcl  14977  invfuc  14986  curf2cl  15143  yonedalem4c  15189  yonedalem3  15192  pospo  15245  latjle12  15334  latjlej1  15337  latnlej2  15343  latlem12  15350  latmlem1  15353  latledi  15361  latmlej11  15362  latjass  15367  latj12  15368  latj32  15369  latj13  15370  latj31  15371  latjrot  15372  latjjdi  15375  latjjdir  15376  latdisdlem  15461  prdsmndd  15556  imasmnd2  15560  frmdmnd  15639  grpsubrcan  15709  grpsubadd  15715  grpsubsub  15716  grpaddsubass  15717  grpsubsub4  15720  grpnnncan2  15723  mulgnndir  15751  mulgnn0dir  15752  mulgdir  15754  mulgnnass  15757  mulgnn0ass  15758  mulgass  15759  mulgsubdir  15760  pwsmulg  15771  imasgrp2  15772  issubg2  15798  eqgval  15832  divsgrp  15838  galcan  15924  gacan  15925  oppgmnd  15971  symggrp  16007  pmtrprfv  16061  pmtr3ncom  16083  psgnunilem3  16104  cmn32  16399  cmn12  16401  abladdsub  16408  mulgnn0di  16417  mulgdi  16418  mulgsubdi  16421  dprdss  16631  dprdz  16632  dprdf1o  16634  dprdsn  16638  dprd2da  16646  ablfac1b  16676  pgpfac1lem5  16685  srgi  16718  srgbinomlem2  16745  srgbinom  16749  rngi  16763  prdsrngd  16810  imasrng  16817  opprrng  16829  mulgass3  16835  dvrass  16888  kerf1hrm  16937  subrgunit  16989  issubrg2  16991  abvdiv  17028  islss3  17146  prdslmodd  17156  islmhm2  17225  lspsolv  17330  islbs2  17341  islbs3  17342  lbsextlem4  17348  sralmod  17374  issubassa  17501  sraassa  17502  psrbaglecl  17543  psrbagcon  17546  psrgrp  17575  psrlmod  17578  psrrng  17590  psrassa  17593  ipdir  18177  ipdi  18178  ipsubdir  18180  ipsubdi  18181  ipass  18183  ipassr  18184  ipassr2  18185  ocvlss  18206  mamudm  18397  matrng  18440  matassa  18441  ofco2  18443  mdetunilem1  18534  mdetunilem9  18542  mdetuni0  18543  mdetmul  18545  gsummatr01lem3  18579  iinopn  18631  subbascn  18974  nrmsep2  19076  isnrm3  19079  regsep2  19096  dnsconst  19098  dfcon2  19139  1stcelcls  19181  nllyidm  19209  dislly  19217  upxp  19312  fbasne0  19519  filss  19542  infil  19552  fsubbas  19556  filssufilg  19600  tmdcn2  19776  psmettri  20003  isxmet2d  20018  xmettri  20042  xmetres2  20052  bldisj  20089  blss2ps  20094  blss2  20095  xmstri2  20157  mstri2  20158  xmstri  20159  mstri  20160  xmstri3  20161  mstri3  20162  msrtri  20163  comet  20204  stdbdbl  20208  met2ndci  20213  ngprcan  20317  ngplcan  20318  ngpsubcan  20321  nrgdsdi  20362  nrgdsdir  20363  nlmdsdi  20378  nlmdsdir  20379  blcvx  20491  icccmplem2  20516  pi1grplem  20737  pi1cof  20747  cvsdiv  20797  cvsdivcl  20798  cphdivcl  20817  cphsubdir  20842  cphsubdi  20843  cphassr  20846  bcthlem5  20955  rrxcph  21012  volfiniun  21144  volcn  21202  itg1val2  21278  dvconst  21507  dvlip  21581  dvfsumlem4  21617  ftc1a  21625  ulmval  21961  ulmdvlem3  21983  ang180  22326  cvxcl  22494  scvxcvx  22495  sgmmul  22656  logexprlim  22680  dchrabl  22709  f1otrge  23253  xmstrkgc  23267  colinearalglem1  23287  colinearalg  23291  axcgrtr  23296  axlowdimlem16  23338  axeuclidlem  23343  axcontlem7  23351  eengtrkg  23366  eengtrkge  23367  wlkoniswlk  23567  constr2trl  23633  wlkdvspth  23642  iseupa  23721  grpodivdiv  23870  grpomuldivass  23871  grpopnpcan2  23875  ablodivdiv4  23913  ablonnncan  23915  ablonnncan1  23917  zerdivemp1  24056  nvmdi  24165  dipassr  24381  archiabllem2c  26346  dvrdir  26392  dvrcan5  26395  reofld  26442  pstmfval  26457  tpr2rico  26476  qqhval2lem  26544  qqhvq  26550  issiga  26688  measdivcstOLD  26772  measdivcst  26773  signsply0  27086  erdszelem9  27221  rescon  27269  cvmseu  27299  cvmlift2lem12  27337  cgrid2  28168  segconeu  28176  btwncomim  28178  btwnswapid  28182  cgrxfr  28220  btwnxfr  28221  colineardim1  28226  brofs2  28242  brifs2  28243  idinside  28249  endofsegid  28250  btwnconn1lem7  28258  btwnconn1lem11  28262  btwnconn1  28266  segcon2  28270  seglemin  28278  segletr  28279  btwnsegle  28282  colinbtwnle  28283  broutsideof2  28287  broutsideof3  28291  outsidele  28297  fvray  28306  fvline  28309  linerflx1  28314  ellines  28317  ftc1anc  28613  ivthALT  28668  sdclem1  28777  sstotbnd2  28811  zerdivemp1x  28899  isdrngo2  28902  iscringd  28937  irrapxlem6  29306  jm2.26lem3  29488  dgrsub2  29629  mpaadgr  29649  mendrng  29687  mendlmod  29688  mendassa  29689  fmuldfeq  29902  stoweidlem43  29976  stoweidlem52  29985  stoweidlem53  29986  stoweidlem56  29989  stoweidlem57  29990  el2spthonot0  30528  el2wlkonotot0  30529  usg2wotspth  30541  2pthwlkonot  30542  erclwwlktr  30623  erclwwlkntr  30639  numclwwlk5  30843  friendship  30853  ply1ass23l  30970  linccl  31055  lincext1  31095  lincext3  31097  lincresunit2  31119  bnj149  32168  bnj1118  32275  bnj1128  32281  lsmsat  32959  lfladdcl  33022  lflnegcl  33026  lflvscl  33028  lshpkrlem4  33064  lshpkrlem6  33066  ldualgrplem  33096  lduallmodlem  33103  latmassOLD  33180  latm12  33181  latm32  33182  latmrot  33183  latmmdiN  33185  latmmdir  33186  omlfh1N  33209  omlfh3N  33210  cvlexchb1  33281  cvlexch3  33283  cvlexch4N  33284  cvlatexchb1  33285  cvlsupr2  33294  hlatjass  33320  hlatj12  33321  hlatj32  33322  cvratlem  33371  cvrat  33372  atcvrj0  33378  cvrat2  33379  atltcvr  33385  atexchltN  33391  cvrat3  33392  cvrat4  33393  3dimlem3  33411  3dimlem3OLDN  33412  3at  33440  2atneat  33465  llncmp  33472  2at0mat0  33475  2atmat0  33476  lplnnle2at  33491  llncvrlpln  33508  lplncmp  33512  lplnexllnN  33514  2llnjaN  33516  4atlem11  33559  lplncvrlvol  33566  lvolcmp  33567  2atm2atN  33735  elpaddatriN  33753  paddasslem9  33778  paddass  33788  padd12N  33789  paddssw2  33794  paddss  33795  pmodlem2  33797  pmodN  33800  pmapjlln1  33805  atmod1i1  33807  atmod1i2  33809  pexmidlem2N  33921  pexmidlem6N  33925  pl42N  33933  lhpm0atN  33979  lautlt  34041  lautcvr  34042  lautj  34043  lautm  34044  ltrneq2  34098  cdlemc3  34143  cdlemc4  34144  cdlemd1  34148  cdleme1b  34176  cdleme1  34177  cdleme2  34178  cdleme3e  34182  cdlemefr27cl  34353  cdlemefs27cl  34363  cdleme42mN  34437  cdlemftr2  34516  trljco  34690  tgrpgrplem  34699  tendoplass  34733  tendodi1  34734  tendodi2  34735  cdlemk36  34863  erngdvlem3  34940  erngdvlem3-rN  34948  tendospdi1  34971  dvalveclem  34976  dialss  34997  dvhvaddass  35048  dvhopvsca  35053  dvhlveclem  35059  diblss  35121  diclss  35144  dihmeetlem12N  35269  dihmeetlem15N  35272  dihmeetlem16N  35273  dihmeetlem17N  35274  dihmeetlem18N  35275  dihmeetlem19N  35276  dvh4dimN  35398  lpolvN  35437  lclkr  35484  lclkrs  35490  lcfr  35536
  Copyright terms: Public domain W3C validator