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

Theorem simpr1 961
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 955 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
21adantl 452 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  simplr1  997  simprr1  1003  simp1r1  1051  simp2r1  1057  simp3r1  1063  3anandis  1283  fr3nr  4571  isopolem  5842  frfi  7102  intrnfi  7170  iinfi  7171  eqsup  7207  fisupcl  7218  cnfcomlem  7402  ackbij1lem15  7860  fpwwe2lem5  8256  ico0  10702  elioc2  10713  elico2  10714  elicc2  10715  iccsplit  10768  fseq1p1m1  10857  ccatswrd  11459  tanadd  12447  dvds2ln  12559  qredeq  12785  ressress  13205  mreexexlem4d  13549  mreexexd  13550  0catg  13589  2oppccomf  13628  issubc3  13723  fthmon  13801  fuccocl  13838  fucidcl  13839  invfuc  13848  curf2cl  14005  yonedalem4c  14051  yonedalem3  14054  pospo  14107  latjlej1  14171  latnlej2  14177  latmlem1  14187  latledi  14195  latmlej11  14196  latjass  14201  latj12  14202  latj32  14203  latj13  14204  latj31  14205  latjrot  14206  latjjdi  14209  latjjdir  14210  latdisdlem  14292  prdsmndd  14405  imasmnd2  14409  frmdmnd  14481  grpsubrcan  14547  grpsubadd  14553  grpsubsub  14554  grpaddsubass  14555  grpsubsub4  14558  grpnnncan2  14561  mulgnndir  14589  mulgnn0dir  14590  mulgdir  14592  mulgnnass  14595  mulgnn0ass  14596  mulgass  14597  mulgsubdir  14598  pwsmulg  14609  imasgrp2  14610  issubg2  14636  eqgval  14666  divsgrp  14672  galcan  14758  gacan  14759  symggrp  14780  oppgmnd  14827  cmn32  15107  cmn12  15109  abladdsub  15116  mulgnn0di  15125  mulgdi  15126  mulgsubdi  15129  dprdss  15264  dprdz  15265  dprdf1o  15267  dprdsn  15271  dprd2da  15277  ablfac1b  15305  pgpfac1lem5  15314  rngi  15353  prdsrngd  15395  imasrng  15402  opprrng  15413  mulgass3  15419  dvrass  15472  subrgunit  15563  issubrg2  15565  abvdiv  15602  islss3  15716  prdslmodd  15726  islmhm2  15795  lspsolv  15896  islbs2  15907  islbs3  15908  lbsextlem4  15914  sralmod  15939  issubassa  16064  sraassa  16065  psrbaglecl  16115  psrbagcon  16117  psrgrp  16143  psrlmod  16146  psrrng  16155  psrassa  16158  ipdir  16543  ipdi  16544  ipsubdir  16546  ipsubdi  16547  ipass  16549  ipassr  16550  ipassr2  16551  ocvlss  16572  iinopn  16648  subbascn  16984  nrmsep2  17084  isnrm3  17087  regsep2  17104  dnsconst  17106  dfcon2  17145  1stcelcls  17187  nllyidm  17215  dislly  17223  upxp  17317  fbasne0  17525  filss  17548  infil  17558  fsubbas  17562  filssufilg  17606  tmdcn2  17772  isxmet2d  17892  xmettri  17915  xmetres2  17925  bldisj  17955  blss2  17959  xmstri2  18012  mstri2  18013  xmstri  18014  mstri  18015  xmstri3  18016  mstri3  18017  msrtri  18018  comet  18059  stdbdbl  18063  met2ndci  18068  ngprcan  18131  ngplcan  18132  ngpsubcan  18135  nrgdsdi  18176  nrgdsdir  18177  nlmdsdi  18192  nlmdsdir  18193  blcvx  18304  icccmplem2  18328  pi1grplem  18547  pi1cof  18557  cphdivcl  18618  cphsubdir  18643  cphsubdi  18644  cphassr  18647  bcthlem5  18750  volfiniun  18904  volcn  18961  itg1val2  19039  dvconst  19266  dvlip  19340  dvfsumlem4  19376  ftc1a  19384  ulmval  19759  ulmdvlem3  19779  ang180  20112  cvxcl  20279  scvxcvx  20280  sgmmul  20440  logexprlim  20464  dchrabl  20493  grpodivdiv  20915  grpomuldivass  20916  grpopnpcan2  20920  ablodivdiv4  20958  ablonnncan  20960  ablonnncan1  20962  nvmdi  21208  dipassr  21424  tpr2rico  23296  issiga  23472  measdivcstOLD  23551  measdivcst  23552  erdszelem9  23730  rescon  23777  cvmseu  23807  cvmlift2lem12  23845  iseupa  23881  dedekindle  24083  colinearalglem1  24534  colinearalg  24538  axcgrtr  24543  axlowdimlem16  24585  axeuclidlem  24590  axcontlem7  24598  cgrid2  24626  segconeu  24634  btwncomim  24636  btwnswapid  24640  cgrxfr  24678  btwnxfr  24679  colineardim1  24684  brofs2  24700  brifs2  24701  idinside  24707  endofsegid  24708  btwnconn1lem7  24716  btwnconn1lem11  24720  btwnconn1  24724  segcon2  24728  seglemin  24736  segletr  24737  btwnsegle  24740  colinbtwnle  24741  broutsideof2  24745  broutsideof3  24749  outsidele  24755  fvray  24764  fvline  24767  linerflx1  24772  ellines  24775  copsexgb  24966  iccss3  25134  reacomsmgrp1  25343  reacomsmgrp2  25344  reacomsmgrp3  25345  grpodrcan  25375  rltrran  25414  zerdivemp1  25436  dblsubvec  25474  mvecrtol2  25477  cnrsfin  25525  cnrscoa  25526  cmptdst  25568  cmptdst2  25571  usinuniopb  25594  lvsovso  25626  lvsovso3  25628  addassv  25656  addcanrg  25667  icccon2  25700  fnctartar  25907  fnctartar2  25908  bosser  26167  ivthALT  26258  sdclem1  26453  sstotbnd2  26498  zerdivemp1x  26586  isdrngo2  26589  iscringd  26624  irrapxlem6  26912  jm2.26lem3  27094  dgrsub2  27339  mpaadgr  27359  pmtrprfv  27396  psgnunilem3  27419  matrng  27480  matassa  27481  mendrng  27500  mendlmod  27501  mendassa  27502  fmuldfeq  27713  stoweidlem43  27792  stoweidlem53  27802  stoweidlem56  27805  stoweidlem57  27806  bnj149  28907  bnj1118  29014  bnj1128  29020  lsmsat  29198  lfladdcl  29261  lflnegcl  29265  lflvscl  29267  lshpkrlem4  29303  lshpkrlem6  29305  ldualgrplem  29335  lduallmodlem  29342  latmassOLD  29419  latm12  29420  latm32  29421  latmrot  29422  latmmdiN  29424  latmmdir  29425  omlfh1N  29448  omlfh3N  29449  cvlexchb1  29520  cvlexch3  29522  cvlexch4N  29523  cvlatexchb1  29524  cvlsupr2  29533  hlatjass  29559  hlatj12  29560  hlatj32  29561  cvratlem  29610  cvrat  29611  atcvrj0  29617  cvrat2  29618  atltcvr  29624  atexchltN  29630  cvrat3  29631  cvrat4  29632  3dimlem3  29650  3dimlem3OLDN  29651  3at  29679  2atneat  29704  llncmp  29711  2at0mat0  29714  2atmat0  29715  lplnnle2at  29730  llncvrlpln  29747  lplncmp  29751  lplnexllnN  29753  2llnjaN  29755  4atlem11  29798  lplncvrlvol  29805  lvolcmp  29806  2atm2atN  29974  elpaddatriN  29992  paddasslem9  30017  paddass  30027  padd12N  30028  paddssw2  30033  paddss  30034  pmodlem2  30036  pmodN  30039  pmapjlln1  30044  atmod1i1  30046  atmod1i2  30048  pexmidlem2N  30160  pexmidlem6N  30164  pl42N  30172  lhpm0atN  30218  lautlt  30280  lautcvr  30281  lautj  30282  lautm  30283  ltrneq2  30337  cdlemc3  30382  cdlemc4  30383  cdlemd1  30387  cdleme1b  30415  cdleme1  30416  cdleme2  30417  cdleme3e  30421  cdlemefr27cl  30592  cdlemefs27cl  30602  cdleme42mN  30676  cdlemftr2  30755  trljco  30929  tgrpgrplem  30938  tendoplass  30972  tendodi1  30973  tendodi2  30974  cdlemk36  31102  erngdvlem3  31179  erngdvlem3-rN  31187  tendospdi1  31210  dvalveclem  31215  dialss  31236  dvhvaddass  31287  dvhopvsca  31292  dvhlveclem  31298  diblss  31360  diclss  31383  dihmeetlem12N  31508  dihmeetlem15N  31511  dihmeetlem16N  31512  dihmeetlem17N  31513  dihmeetlem18N  31514  dihmeetlem19N  31515  dvh4dimN  31637  lpolvN  31676  lclkr  31723  lclkrs  31729  lcfr  31775
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator