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

Theorem simpr1 1001
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 995 . 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 972
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 974
This theorem is referenced by:  simplr1  1037  simprr1  1043  simp1r1  1091  simp2r1  1097  simp3r1  1103  3anandis  1329  isopolem  6223  fr3nr  6597  suppfnss  6924  frfi  7764  intrnfi  7875  iinfi  7876  eqsup  7915  fisupcl  7927  cnfcomlem  8143  cnfcomlemOLD  8151  ackbij1lem15  8614  fpwwe2lem5  9012  dedekindle  9745  ico0  11581  elioc2  11593  elico2  11594  elicc2  11595  iccsplit  11659  fseq1p1m1  11758  elfz0ubfz0  11783  hashtpg  12499  swrdsymbeq  12648  ccatswrd  12657  tanadd  13776  dvds2ln  13888  qredeq  14121  ressress  14568  mreexexlem4d  14918  mreexexd  14919  0catg  14958  2oppccomf  14994  issubc3  15089  fthmon  15167  fuccocl  15204  fucidcl  15205  invfuc  15214  curf2cl  15371  yonedalem4c  15417  yonedalem3  15420  pospo  15474  latjle12  15563  latjlej1  15566  latnlej2  15572  latlem12  15579  latmlem1  15582  latledi  15590  latmlej11  15591  latjass  15596  latj12  15597  latj32  15598  latj13  15599  latj31  15600  latjrot  15601  latjjdi  15604  latjjdir  15605  latdisdlem  15690  prdsmndd  15824  imasmnd2  15828  frmdmnd  15898  grpsubrcan  15990  grpsubadd  15997  grpsubsub  15998  grpaddsubass  15999  grpsubsub4  16002  grpnnncan2  16006  mulgnndir  16035  mulgnn0dir  16036  mulgdir  16038  mulgnnass  16041  mulgnn0ass  16042  mulgass  16043  mulgsubdir  16044  pwsmulg  16055  imasgrp2  16056  issubg2  16087  eqgval  16121  qusgrp  16127  galcan  16213  gacan  16214  oppgmnd  16260  symggrp  16296  pmtrprfv  16349  pmtr3ncom  16371  psgnunilem3  16392  cmn32  16687  cmn12  16689  abladdsub  16696  mulgnn0di  16705  mulgdi  16706  mulgsubdi  16709  dprdss  16947  dprdz  16948  dprdf1o  16950  dprdsn  16954  dprd2da  16962  ablfac1b  16992  pgpfac1lem5  17001  srgbinomlem2  17063  srgbinom  17067  ringi  17082  prdsringd  17132  imasring  17139  opprring  17151  mulgass3  17157  dvrass  17210  kerf1hrm  17263  subrgunit  17318  issubrg2  17320  abvdiv  17357  islss3  17476  prdslmodd  17486  islmhm2  17555  lspsolv  17660  islbs2  17671  islbs3  17672  lbsextlem4  17678  sralmod  17704  issubassa  17844  sraassa  17845  psrbaglecl  17890  psrbagcon  17893  psrgrp  17922  psrlmod  17925  psrring  17937  psrassa  17940  ipdir  18544  ipdi  18545  ipsubdir  18547  ipsubdi  18548  ipass  18550  ipassr  18551  ipassr2  18552  ocvlss  18573  mamudm  18760  matring  18815  matassa  18816  ofco2  18823  mdetunilem1  18984  mdetunilem9  18992  mdetuni0  18993  mdetmul  18995  gsummatr01lem3  19029  iinopn  19281  subbascn  19625  nrmsep2  19727  isnrm3  19730  regsep2  19747  dnsconst  19749  dfcon2  19790  1stcelcls  19832  nllyidm  19860  dislly  19868  upxp  19994  fbasne0  20201  filss  20224  infil  20234  fsubbas  20238  filssufilg  20282  tmdcn2  20458  psmettri  20685  isxmet2d  20700  xmettri  20724  xmetres2  20734  bldisj  20771  blss2ps  20776  blss2  20777  xmstri2  20839  mstri2  20840  xmstri  20841  mstri  20842  xmstri3  20843  mstri3  20844  msrtri  20845  comet  20886  stdbdbl  20890  met2ndci  20895  ngprcan  20999  ngplcan  21000  ngpsubcan  21003  nrgdsdi  21044  nrgdsdir  21045  nlmdsdi  21060  nlmdsdir  21061  blcvx  21173  icccmplem2  21198  pi1grplem  21419  pi1cof  21429  cvsdiv  21479  cvsdivcl  21480  cphdivcl  21499  cphsubdir  21524  cphsubdi  21525  cphassr  21528  bcthlem5  21637  rrxcph  21694  volfiniun  21827  volcn  21885  itg1val2  21961  dvconst  22190  dvlip  22264  dvfsumlem4  22300  ftc1a  22308  ulmval  22644  ulmdvlem3  22666  ang180  23015  cvxcl  23183  scvxcvx  23184  sgmmul  23345  logexprlim  23369  dchrabl  23398  motgrp  23799  f1otrge  24044  colinearalglem1  24078  colinearalg  24082  axcgrtr  24087  axlowdimlem16  24129  axeuclidlem  24134  axcontlem7  24142  eengtrkg  24157  eengtrkge  24158  wlkoniswlk  24405  constr2trl  24470  wlkdvspth  24479  erclwwlktr  24684  erclwwlkntr  24696  el2spthonot0  24740  el2wlkonotot0  24741  usg2wotspth  24753  2pthwlkonot  24754  iseupa  24834  numclwwlk5  24981  friendship  24991  grpodivdiv  25119  grpomuldivass  25120  grpopnpcan2  25124  ablodivdiv4  25162  ablonnncan  25164  ablonnncan1  25166  zerdivemp1  25305  nvmdi  25414  dipassr  25630  archiabllem2c  27609  dvrdir  27650  dvrcan5  27653  reofld  27700  pstmfval  27745  tpr2rico  27764  qqhval2lem  27832  qqhvq  27838  issiga  27981  measdivcstOLD  28065  measdivcst  28066  signsply0  28378  erdszelem9  28513  rescon  28561  cvmseu  28591  cvmlift2lem12  28629  elmrsubrn  28750  mclsind  28800  cgrid2  29625  segconeu  29633  btwncomim  29635  btwnswapid  29639  cgrxfr  29677  btwnxfr  29678  colineardim1  29683  brofs2  29699  brifs2  29700  idinside  29706  endofsegid  29707  btwnconn1lem7  29715  btwnconn1lem11  29719  btwnconn1  29723  segcon2  29727  seglemin  29735  segletr  29736  btwnsegle  29739  colinbtwnle  29740  broutsideof2  29744  broutsideof3  29748  outsidele  29754  fvray  29763  fvline  29766  linerflx1  29771  ellines  29774  ftc1anc  30070  ivthALT  30125  sdclem1  30208  sstotbnd2  30242  zerdivemp1x  30330  isdrngo2  30333  iscringd  30368  irrapxlem6  30735  jm2.26lem3  30915  dgrsub2  31056  mpaadgr  31076  mendring  31114  mendlmod  31115  mendassa  31116  fmuldfeq  31505  stoweidlem43  31714  stoweidlem52  31723  stoweidlem53  31724  stoweidlem56  31727  stoweidlem57  31728  usgfis  32284  usgfisALT  32288  copissgrp  32333  cznrng  32470  funcringcsetcOLD2lem9  32584  funcringcsetclem9OLD  32607  ply1ass23l  32712  linccl  32745  lincext1  32785  lincext3  32787  lincresunit2  32809  bnj149  33661  bnj1118  33768  bnj1128  33774  lsmsat  34456  lfladdcl  34519  lflnegcl  34523  lflvscl  34525  lshpkrlem4  34561  lshpkrlem6  34563  ldualgrplem  34593  lduallmodlem  34600  latmassOLD  34677  latm12  34678  latm32  34679  latmrot  34680  latmmdiN  34682  latmmdir  34683  omlfh1N  34706  omlfh3N  34707  cvlexchb1  34778  cvlexch3  34780  cvlexch4N  34781  cvlatexchb1  34782  cvlsupr2  34791  hlatjass  34817  hlatj12  34818  hlatj32  34819  cvratlem  34868  cvrat  34869  atcvrj0  34875  cvrat2  34876  atltcvr  34882  atexchltN  34888  cvrat3  34889  cvrat4  34890  3dimlem3  34908  3dimlem3OLDN  34909  3at  34937  2atneat  34962  llncmp  34969  2at0mat0  34972  2atmat0  34973  lplnnle2at  34988  llncvrlpln  35005  lplncmp  35009  lplnexllnN  35011  2llnjaN  35013  4atlem11  35056  lplncvrlvol  35063  lvolcmp  35064  2atm2atN  35232  elpaddatriN  35250  paddasslem9  35275  paddass  35285  padd12N  35286  paddssw2  35291  paddss  35292  pmodlem2  35294  pmodN  35297  pmapjlln1  35302  atmod1i1  35304  atmod1i2  35306  pexmidlem2N  35418  pexmidlem6N  35422  pl42N  35430  lhpm0atN  35476  lautlt  35538  lautcvr  35539  lautj  35540  lautm  35541  ltrneq2  35595  cdlemc3  35641  cdlemc4  35642  cdlemd1  35646  cdleme1b  35674  cdleme1  35675  cdleme2  35676  cdleme3e  35680  cdlemefr27cl  35852  cdlemefs27cl  35862  cdleme42mN  35936  cdlemftr2  36015  trljco  36189  tgrpgrplem  36198  tendoplass  36232  tendodi1  36233  tendodi2  36234  cdlemk36  36362  erngdvlem3  36439  erngdvlem3-rN  36447  tendospdi1  36470  dvalveclem  36475  dialss  36496  dvhvaddass  36547  dvhopvsca  36552  dvhlveclem  36558  diblss  36620  diclss  36643  dihmeetlem12N  36768  dihmeetlem15N  36771  dihmeetlem16N  36772  dihmeetlem17N  36773  dihmeetlem18N  36774  dihmeetlem19N  36775  dvh4dimN  36897  lpolvN  36936  lclkr  36983  lclkrs  36989  lcfr  37035
  Copyright terms: Public domain W3C validator