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

Theorem simpr1 1036
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 1030 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
21adantl 473 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    /\ w3a 1007
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 190  df-an 378  df-3an 1009
This theorem is referenced by:  simplr1  1072  simprr1  1078  simp1r1  1126  simp2r1  1132  simp3r1  1138  3anandis  1399  fpr2g  6142  isopolem  6254  fr3nr  6625  suppfnss  6959  frfi  7834  intrnfi  7948  iinfi  7949  eqsup  7988  fisupcl  8003  cnfcomlem  8222  ackbij1lem15  8682  fpwwe2lem5  9077  dedekindle  9816  ico0  11707  elioc2  11722  elico2  11723  elicc2  11724  iccsplit  11791  fseq1p1m1  11894  elfz0ubfz0  11920  hashtpg  12682  swrdsbslen  12858  swrdspsleq  12859  ccatswrd  12866  tanadd  14298  dvds2ln  14410  qredeq  14742  ressress  15265  mreexexlem4d  15631  mreexexd  15632  0catg  15671  2oppccomf  15708  issubc3  15832  fthmon  15910  fuccocl  15947  fucidcl  15948  invfuc  15957  initoeu2lem0  15986  initoeu2lem1  15987  curf2cl  16194  yonedalem4c  16240  yonedalem3  16243  pospo  16297  latjle12  16386  latjlej1  16389  latnlej2  16395  latlem12  16402  latmlem1  16405  latledi  16413  latmlej11  16414  latjass  16419  latj12  16420  latj32  16421  latj13  16422  latj31  16423  latjrot  16424  latjjdi  16427  latjjdir  16428  latdisdlem  16513  prdsmndd  16647  imasmnd2  16651  frmdmnd  16721  grpsubrcan  16813  grpsubadd  16820  grpsubsub  16821  grpaddsubass  16822  grpsubsub4  16825  grpnnncan2  16829  mulgnndir  16858  mulgnn0dir  16859  mulgdir  16861  mulgnnass  16864  mulgnn0ass  16865  mulgass  16866  mulgsubdir  16867  pwsmulg  16878  imasgrp2  16879  issubg2  16910  eqgval  16944  qusgrp  16950  galcan  17036  gacan  17037  oppgmnd  17083  symggrp  17119  pmtrprfv  17172  pmtr3ncom  17194  psgnunilem3  17215  cmn32  17526  cmn12  17528  abladdsub  17535  mulgnn0di  17544  mulgdi  17545  mulgsubdi  17548  dprdss  17740  dprdz  17741  dprdf1o  17743  dprdsn  17747  dprd2da  17753  ablfac1b  17781  pgpfac1lem5  17790  srgbinomlem2  17852  srgbinom  17856  ringi  17871  prdsringd  17918  imasring  17925  opprring  17937  mulgass3  17943  dvrass  17996  kerf1hrm  18049  subrgunit  18104  issubrg2  18106  abvdiv  18143  islss3  18260  prdslmodd  18270  islmhm2  18339  lspsolv  18444  islbs2  18455  islbs3  18456  lbsextlem4  18462  sralmod  18488  issubassa  18625  sraassa  18626  psrbaglecl  18670  psrbagcon  18672  psrgrp  18699  psrlmod  18702  psrring  18712  psrassa  18715  ipdir  19283  ipdi  19284  ipsubdir  19286  ipsubdi  19287  ipass  19289  ipassr  19290  ipassr2  19291  ocvlss  19312  mamudm  19490  matring  19545  matassa  19546  ofco2  19553  mdetunilem1  19714  mdetunilem9  19722  mdetuni0  19723  mdetmul  19725  gsummatr01lem3  19759  iinopn  20009  subbascn  20347  nrmsep2  20449  isnrm3  20452  regsep2  20469  dnsconst  20471  dfcon2  20511  1stcelcls  20553  nllyidm  20581  dislly  20589  upxp  20715  fbasne0  20923  filss  20946  infil  20956  fsubbas  20960  filssufilg  21004  tmdcn2  21182  psmettri  21405  isxmet2d  21420  xmettri  21444  xmetres2  21454  bldisj  21491  blss2ps  21496  blss2  21497  xmstri2  21559  mstri2  21560  xmstri  21561  mstri  21562  xmstri3  21563  mstri3  21564  msrtri  21565  comet  21606  stdbdbl  21610  met2ndci  21615  ngprcan  21701  ngplcan  21702  ngpsubcan  21705  nrgdsdi  21746  nrgdsdir  21747  nlmdsdi  21762  nlmdsdir  21763  blcvx  21894  icccmplem2  21919  pi1grplem  22158  pi1cof  22168  cvsdiv  22218  cvsdivcl  22219  cphdivcl  22238  cphsubdir  22263  cphsubdi  22264  cphassr  22267  bcthlem5  22374  rrxcph  22429  volfiniun  22579  volcn  22643  itg1val2  22721  dvconst  22950  dvlip  23024  dvfsumlem4  23060  ftc1a  23068  ulmval  23414  ulmdvlem3  23436  ang180  23822  cvxcl  23989  scvxcvx  23990  sgmmul  24208  logexprlim  24232  dchrabl  24261  motgrp  24667  iscgra1  24931  cgrane1  24933  cgrane2  24934  cgrahl1  24937  cgrahl2  24938  cgracgr  24939  cgratr  24944  cgrabtwn  24946  dfcgra2  24950  sacgr  24951  f1otrge  24981  colinearalglem1  25015  colinearalg  25019  axcgrtr  25024  axlowdimlem16  25066  axeuclidlem  25071  axcontlem7  25079  eengtrkg  25094  eengtrkge  25095  wlkoniswlk  25343  constr2trl  25408  wlkdvspth  25417  erclwwlktr  25622  erclwwlkntr  25634  el2spthonot0  25678  el2wlkonotot0  25679  usg2wotspth  25691  2pthwlkonot  25692  iseupa  25772  numclwwlk5  25919  friendship  25929  grpodivdiv  26057  grpomuldivass  26058  grpopnpcan2  26062  ablodivdiv4  26100  ablonnncan  26102  ablonnncan1  26104  zerdivemp1  26243  nvmdi  26352  dipassr  26568  archiabllem2c  28586  dvrdir  28627  dvrcan5  28630  reofld  28677  pstmfval  28773  tpr2rico  28792  qqhval2lem  28859  qqhvq  28865  issiga  29007  measdivcstOLD  29120  measdivcst  29121  carsggect  29223  signsply0  29512  bnj149  29758  bnj1118  29865  bnj1128  29871  erdszelem9  29994  rescon  30041  cvmseu  30071  cvmlift2lem12  30109  elmrsubrn  30230  mclsind  30280  cgrid2  30841  segconeu  30849  btwncomim  30851  btwnswapid  30855  cgrxfr  30893  btwnxfr  30894  colineardim1  30899  brofs2  30915  brifs2  30916  idinside  30922  endofsegid  30923  btwnconn1lem7  30931  btwnconn1lem11  30935  btwnconn1  30939  segcon2  30943  seglemin  30951  segletr  30952  btwnsegle  30955  colinbtwnle  30956  broutsideof2  30960  broutsideof3  30964  outsidele  30970  fvray  30979  fvline  30982  linerflx1  30987  ellines  30990  ivthALT  31062  poimirlem32  32036  ftc1anc  32089  sdclem1  32136  sstotbnd2  32170  zerdivemp1x  32258  isdrngo2  32261  iscringd  32296  lsmsat  32645  lfladdcl  32708  lflnegcl  32712  lflvscl  32714  lshpkrlem4  32750  lshpkrlem6  32752  ldualgrplem  32782  lduallmodlem  32789  latmassOLD  32866  latm12  32867  latm32  32868  latmrot  32869  latmmdiN  32871  latmmdir  32872  omlfh1N  32895  omlfh3N  32896  cvlexchb1  32967  cvlexch3  32969  cvlexch4N  32970  cvlatexchb1  32971  cvlsupr2  32980  hlatjass  33006  hlatj12  33007  hlatj32  33008  cvratlem  33057  cvrat  33058  atcvrj0  33064  cvrat2  33065  atltcvr  33071  atexchltN  33077  cvrat3  33078  cvrat4  33079  3dimlem3  33097  3dimlem3OLDN  33098  3at  33126  2atneat  33151  llncmp  33158  2at0mat0  33161  2atmat0  33162  lplnnle2at  33177  llncvrlpln  33194  lplncmp  33198  lplnexllnN  33200  2llnjaN  33202  4atlem11  33245  lplncvrlvol  33252  lvolcmp  33253  2atm2atN  33421  elpaddatriN  33439  paddasslem9  33464  paddass  33474  padd12N  33475  paddssw2  33480  paddss  33481  pmodlem2  33483  pmodN  33486  pmapjlln1  33491  atmod1i1  33493  atmod1i2  33495  pexmidlem2N  33607  pexmidlem6N  33611  pl42N  33619  lhpm0atN  33665  lautlt  33727  lautcvr  33728  lautj  33729  lautm  33730  ltrneq2  33784  cdlemc3  33830  cdlemc4  33831  cdlemd1  33835  cdleme1b  33863  cdleme1  33864  cdleme2  33865  cdleme3e  33869  cdlemefr27cl  34041  cdlemefs27cl  34051  cdleme42mN  34125  cdlemftr2  34204  trljco  34378  tgrpgrplem  34387  tendoplass  34421  tendodi1  34422  tendodi2  34423  cdlemk36  34551  erngdvlem3  34628  erngdvlem3-rN  34636  tendospdi1  34659  dvalveclem  34664  dialss  34685  dvhvaddass  34736  dvhopvsca  34741  dvhlveclem  34747  diblss  34809  diclss  34832  dihmeetlem12N  34957  dihmeetlem15N  34960  dihmeetlem16N  34961  dihmeetlem17N  34962  dihmeetlem18N  34963  dihmeetlem19N  34964  dvh4dimN  35086  lpolvN  35125  lclkr  35172  lclkrs  35178  lcfr  35224  irrapxlem6  35742  jm2.26lem3  35927  dgrsub2  36065  mpaadgr  36091  mendring  36129  mendlmod  36130  mendassa  36131  relexpmulg  36373  iunrelexpmin2  36375  relexpxpmin  36380  fmuldfeq  37758  stoweidlem43  38016  stoweidlem52  38025  stoweidlem53  38026  stoweidlem56  38029  stoweidlem57  38030  nbfusgrlevtxm2  39616  upgr1wlkwlk  39842  lfgriswlk  39880  upgrwlkdvde  39929  usgfis  40266  usgfisALT  40270  copissgrp  40316  cznrng  40465  funcringcsetcALTV2lem9  40554  funcringcsetclem9ALTV  40577  ply1ass23l  40682  linccl  40715  lincext1  40755  lincext3  40757  lincresunit2  40779
  Copyright terms: Public domain W3C validator