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

Theorem simpr1 1011
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 1005 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
21adantl 467 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  simplr1  1047  simprr1  1053  simp1r1  1101  simp2r1  1107  simp3r1  1113  3anandis  1366  fpr2g  6137  isopolem  6248  fr3nr  6617  suppfnss  6948  frfi  7819  intrnfi  7933  iinfi  7934  eqsup  7973  fisupcl  7988  cnfcomlem  8206  ackbij1lem15  8665  fpwwe2lem5  9060  dedekindle  9799  ico0  11683  elioc2  11698  elico2  11699  elicc2  11700  iccsplit  11766  fseq1p1m1  11869  elfz0ubfz0  11895  hashtpg  12638  swrdsbslen  12795  swrdspsleq  12796  ccatswrd  12803  tanadd  14209  dvds2ln  14321  qredeq  14651  ressress  15175  mreexexlem4d  15541  mreexexd  15542  0catg  15581  2oppccomf  15618  issubc3  15742  fthmon  15820  fuccocl  15857  fucidcl  15858  invfuc  15867  initoeu2lem0  15896  initoeu2lem1  15897  curf2cl  16104  yonedalem4c  16150  yonedalem3  16153  pospo  16207  latjle12  16296  latjlej1  16299  latnlej2  16305  latlem12  16312  latmlem1  16315  latledi  16323  latmlej11  16324  latjass  16329  latj12  16330  latj32  16331  latj13  16332  latj31  16333  latjrot  16334  latjjdi  16337  latjjdir  16338  latdisdlem  16423  prdsmndd  16557  imasmnd2  16561  frmdmnd  16631  grpsubrcan  16723  grpsubadd  16730  grpsubsub  16731  grpaddsubass  16732  grpsubsub4  16735  grpnnncan2  16739  mulgnndir  16768  mulgnn0dir  16769  mulgdir  16771  mulgnnass  16774  mulgnn0ass  16775  mulgass  16776  mulgsubdir  16777  pwsmulg  16788  imasgrp2  16789  issubg2  16820  eqgval  16854  qusgrp  16860  galcan  16946  gacan  16947  oppgmnd  16993  symggrp  17029  pmtrprfv  17082  pmtr3ncom  17104  psgnunilem3  17125  cmn32  17436  cmn12  17438  abladdsub  17445  mulgnn0di  17454  mulgdi  17455  mulgsubdi  17458  dprdss  17650  dprdz  17651  dprdf1o  17653  dprdsn  17657  dprd2da  17663  ablfac1b  17691  pgpfac1lem5  17700  srgbinomlem2  17762  srgbinom  17766  ringi  17781  prdsringd  17828  imasring  17835  opprring  17847  mulgass3  17853  dvrass  17906  kerf1hrm  17959  subrgunit  18014  issubrg2  18016  abvdiv  18053  islss3  18170  prdslmodd  18180  islmhm2  18249  lspsolv  18354  islbs2  18365  islbs3  18366  lbsextlem4  18372  sralmod  18398  issubassa  18536  sraassa  18537  psrbaglecl  18581  psrbagcon  18583  psrgrp  18610  psrlmod  18613  psrring  18623  psrassa  18626  ipdir  19193  ipdi  19194  ipsubdir  19196  ipsubdi  19197  ipass  19199  ipassr  19200  ipassr2  19201  ocvlss  19222  mamudm  19400  matring  19455  matassa  19456  ofco2  19463  mdetunilem1  19624  mdetunilem9  19632  mdetuni0  19633  mdetmul  19635  gsummatr01lem3  19669  iinopn  19919  subbascn  20257  nrmsep2  20359  isnrm3  20362  regsep2  20379  dnsconst  20381  dfcon2  20421  1stcelcls  20463  nllyidm  20491  dislly  20499  upxp  20625  fbasne0  20832  filss  20855  infil  20865  fsubbas  20869  filssufilg  20913  tmdcn2  21091  psmettri  21314  isxmet2d  21329  xmettri  21353  xmetres2  21363  bldisj  21400  blss2ps  21405  blss2  21406  xmstri2  21468  mstri2  21469  xmstri  21470  mstri  21471  xmstri3  21472  mstri3  21473  msrtri  21474  comet  21515  stdbdbl  21519  met2ndci  21524  ngprcan  21610  ngplcan  21611  ngpsubcan  21614  nrgdsdi  21655  nrgdsdir  21656  nlmdsdi  21671  nlmdsdir  21672  blcvx  21803  icccmplem2  21828  pi1grplem  22067  pi1cof  22077  cvsdiv  22127  cvsdivcl  22128  cphdivcl  22147  cphsubdir  22172  cphsubdi  22173  cphassr  22176  bcthlem5  22283  rrxcph  22338  volfiniun  22487  volcn  22551  itg1val2  22629  dvconst  22858  dvlip  22932  dvfsumlem4  22968  ftc1a  22976  ulmval  23322  ulmdvlem3  23344  ang180  23730  cvxcl  23897  scvxcvx  23898  sgmmul  24116  logexprlim  24140  dchrabl  24169  motgrp  24575  iscgra1  24839  cgrane1  24841  cgrane2  24842  cgrahl1  24845  cgrahl2  24846  cgracgr  24847  cgratr  24852  cgrabtwn  24854  dfcgra2  24858  sacgr  24859  f1otrge  24889  colinearalglem1  24923  colinearalg  24927  axcgrtr  24932  axlowdimlem16  24974  axeuclidlem  24979  axcontlem7  24987  eengtrkg  25002  eengtrkge  25003  wlkoniswlk  25250  constr2trl  25315  wlkdvspth  25324  erclwwlktr  25529  erclwwlkntr  25541  el2spthonot0  25585  el2wlkonotot0  25586  usg2wotspth  25598  2pthwlkonot  25599  iseupa  25679  numclwwlk5  25826  friendship  25836  grpodivdiv  25962  grpomuldivass  25963  grpopnpcan2  25967  ablodivdiv4  26005  ablonnncan  26007  ablonnncan1  26009  zerdivemp1  26148  nvmdi  26257  dipassr  26473  archiabllem2c  28507  dvrdir  28549  dvrcan5  28552  reofld  28599  pstmfval  28695  tpr2rico  28714  qqhval2lem  28781  qqhvq  28787  issiga  28929  measdivcstOLD  29042  measdivcst  29043  carsggect  29146  signsply0  29436  bnj149  29682  bnj1118  29789  bnj1128  29795  erdszelem9  29918  rescon  29965  cvmseu  29995  cvmlift2lem12  30033  elmrsubrn  30154  mclsind  30204  cgrid2  30763  segconeu  30771  btwncomim  30773  btwnswapid  30777  cgrxfr  30815  btwnxfr  30816  colineardim1  30821  brofs2  30837  brifs2  30838  idinside  30844  endofsegid  30845  btwnconn1lem7  30853  btwnconn1lem11  30857  btwnconn1  30861  segcon2  30865  seglemin  30873  segletr  30874  btwnsegle  30877  colinbtwnle  30878  broutsideof2  30882  broutsideof3  30886  outsidele  30892  fvray  30901  fvline  30904  linerflx1  30909  ellines  30912  ivthALT  30984  poimirlem32  31886  ftc1anc  31939  sdclem1  31986  sstotbnd2  32020  zerdivemp1x  32108  isdrngo2  32111  iscringd  32146  lsmsat  32493  lfladdcl  32556  lflnegcl  32560  lflvscl  32562  lshpkrlem4  32598  lshpkrlem6  32600  ldualgrplem  32630  lduallmodlem  32637  latmassOLD  32714  latm12  32715  latm32  32716  latmrot  32717  latmmdiN  32719  latmmdir  32720  omlfh1N  32743  omlfh3N  32744  cvlexchb1  32815  cvlexch3  32817  cvlexch4N  32818  cvlatexchb1  32819  cvlsupr2  32828  hlatjass  32854  hlatj12  32855  hlatj32  32856  cvratlem  32905  cvrat  32906  atcvrj0  32912  cvrat2  32913  atltcvr  32919  atexchltN  32925  cvrat3  32926  cvrat4  32927  3dimlem3  32945  3dimlem3OLDN  32946  3at  32974  2atneat  32999  llncmp  33006  2at0mat0  33009  2atmat0  33010  lplnnle2at  33025  llncvrlpln  33042  lplncmp  33046  lplnexllnN  33048  2llnjaN  33050  4atlem11  33093  lplncvrlvol  33100  lvolcmp  33101  2atm2atN  33269  elpaddatriN  33287  paddasslem9  33312  paddass  33322  padd12N  33323  paddssw2  33328  paddss  33329  pmodlem2  33331  pmodN  33334  pmapjlln1  33339  atmod1i1  33341  atmod1i2  33343  pexmidlem2N  33455  pexmidlem6N  33459  pl42N  33467  lhpm0atN  33513  lautlt  33575  lautcvr  33576  lautj  33577  lautm  33578  ltrneq2  33632  cdlemc3  33678  cdlemc4  33679  cdlemd1  33683  cdleme1b  33711  cdleme1  33712  cdleme2  33713  cdleme3e  33717  cdlemefr27cl  33889  cdlemefs27cl  33899  cdleme42mN  33973  cdlemftr2  34052  trljco  34226  tgrpgrplem  34235  tendoplass  34269  tendodi1  34270  tendodi2  34271  cdlemk36  34399  erngdvlem3  34476  erngdvlem3-rN  34484  tendospdi1  34507  dvalveclem  34512  dialss  34533  dvhvaddass  34584  dvhopvsca  34589  dvhlveclem  34595  diblss  34657  diclss  34680  dihmeetlem12N  34805  dihmeetlem15N  34808  dihmeetlem16N  34809  dihmeetlem17N  34810  dihmeetlem18N  34811  dihmeetlem19N  34812  dvh4dimN  34934  lpolvN  34973  lclkr  35020  lclkrs  35026  lcfr  35072  irrapxlem6  35591  jm2.26lem3  35776  dgrsub2  35914  mpaadgr  35940  mendring  35978  mendlmod  35979  mendassa  35980  relexpmulg  36162  iunrelexpmin2  36164  relexpxpmin  36169  fmuldfeq  37481  stoweidlem43  37724  stoweidlem52  37733  stoweidlem53  37734  stoweidlem56  37737  stoweidlem57  37738  usgfis  39030  usgfisALT  39034  copissgrp  39080  cznrng  39229  funcringcsetcALTV2lem9  39318  funcringcsetclem9ALTV  39341  ply1ass23l  39448  linccl  39481  lincext1  39521  lincext3  39523  lincresunit2  39545
  Copyright terms: Public domain W3C validator