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

Theorem simpr1 964
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 958 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
21adantl 454 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  simplr1  1000  simprr1  1006  simp1r1  1054  simp2r1  1060  simp3r1  1066  3anandis  1286  fr3nr  4763  isopolem  6068  frfi  7355  intrnfi  7424  iinfi  7425  eqsup  7464  fisupcl  7475  cnfcomlem  7659  ackbij1lem15  8119  fpwwe2lem5  8514  ico0  10967  elioc2  10978  elico2  10979  elicc2  10980  iccsplit  11034  fseq1p1m1  11127  hashtpg  11696  ccatswrd  11778  tanadd  12773  dvds2ln  12885  qredeq  13111  ressress  13531  mreexexlem4d  13877  mreexexd  13878  0catg  13917  2oppccomf  13956  issubc3  14051  fthmon  14129  fuccocl  14166  fucidcl  14167  invfuc  14176  curf2cl  14333  yonedalem4c  14379  yonedalem3  14382  pospo  14435  latjlej1  14499  latnlej2  14505  latmlem1  14515  latledi  14523  latmlej11  14524  latjass  14529  latj12  14530  latj32  14531  latj13  14532  latj31  14533  latjrot  14534  latjjdi  14537  latjjdir  14538  latdisdlem  14620  prdsmndd  14733  imasmnd2  14737  frmdmnd  14809  grpsubrcan  14875  grpsubadd  14881  grpsubsub  14882  grpaddsubass  14883  grpsubsub4  14886  grpnnncan2  14889  mulgnndir  14917  mulgnn0dir  14918  mulgdir  14920  mulgnnass  14923  mulgnn0ass  14924  mulgass  14925  mulgsubdir  14926  pwsmulg  14937  imasgrp2  14938  issubg2  14964  eqgval  14994  divsgrp  15000  galcan  15086  gacan  15087  symggrp  15108  oppgmnd  15155  cmn32  15435  cmn12  15437  abladdsub  15444  mulgnn0di  15453  mulgdi  15454  mulgsubdi  15457  dprdss  15592  dprdz  15593  dprdf1o  15595  dprdsn  15599  dprd2da  15605  ablfac1b  15633  pgpfac1lem5  15642  rngi  15681  prdsrngd  15723  imasrng  15730  opprrng  15741  mulgass3  15747  dvrass  15800  subrgunit  15891  issubrg2  15893  abvdiv  15930  islss3  16040  prdslmodd  16050  islmhm2  16119  lspsolv  16220  islbs2  16231  islbs3  16232  lbsextlem4  16238  sralmod  16263  issubassa  16388  sraassa  16389  psrbaglecl  16439  psrbagcon  16441  psrgrp  16467  psrlmod  16470  psrrng  16479  psrassa  16482  ipdir  16875  ipdi  16876  ipsubdir  16878  ipsubdi  16879  ipass  16881  ipassr  16882  ipassr2  16883  ocvlss  16904  iinopn  16980  subbascn  17323  nrmsep2  17425  isnrm3  17428  regsep2  17445  dnsconst  17447  dfcon2  17487  1stcelcls  17529  nllyidm  17557  dislly  17565  upxp  17660  fbasne0  17867  filss  17890  infil  17900  fsubbas  17904  filssufilg  17948  tmdcn2  18124  psmettri  18347  isxmet2d  18362  xmettri  18386  xmetres2  18396  bldisj  18433  blss2ps  18438  blss2  18439  xmstri2  18501  mstri2  18502  xmstri  18503  mstri  18504  xmstri3  18505  mstri3  18506  msrtri  18507  comet  18548  stdbdbl  18552  met2ndci  18557  ngprcan  18661  ngplcan  18662  ngpsubcan  18665  nrgdsdi  18706  nrgdsdir  18707  nlmdsdi  18722  nlmdsdir  18723  blcvx  18834  icccmplem2  18859  pi1grplem  19079  pi1cof  19089  cphdivcl  19150  cphsubdir  19175  cphsubdi  19176  cphassr  19179  bcthlem5  19286  volfiniun  19446  volcn  19503  itg1val2  19579  dvconst  19808  dvlip  19882  dvfsumlem4  19918  ftc1a  19926  ulmval  20301  ulmdvlem3  20323  ang180  20661  cvxcl  20828  scvxcvx  20829  sgmmul  20990  logexprlim  21014  dchrabl  21043  wlkoniswlk  21538  constr2trl  21604  wlkdvspth  21613  iseupa  21692  grpodivdiv  21841  grpomuldivass  21842  grpopnpcan2  21846  ablodivdiv4  21884  ablonnncan  21886  ablonnncan1  21888  zerdivemp1  22027  nvmdi  22136  dipassr  22352  dvrdir  24231  dvrcan5  24234  kerf1hrm  24267  reofld  24285  pstmfval  24296  tpr2rico  24315  qqhval2lem  24370  qqhvq  24376  issiga  24499  measdivcstOLD  24583  measdivcst  24584  erdszelem9  24890  rescon  24938  cvmseu  24968  cvmlift2lem12  25006  dedekindle  25193  colinearalglem1  25850  colinearalg  25854  axcgrtr  25859  axlowdimlem16  25901  axeuclidlem  25906  axcontlem7  25914  cgrid2  25942  segconeu  25950  btwncomim  25952  btwnswapid  25956  cgrxfr  25994  btwnxfr  25995  colineardim1  26000  brofs2  26016  brifs2  26017  idinside  26023  endofsegid  26024  btwnconn1lem7  26032  btwnconn1lem11  26036  btwnconn1  26040  segcon2  26044  seglemin  26052  segletr  26053  btwnsegle  26056  colinbtwnle  26057  broutsideof2  26061  broutsideof3  26065  outsidele  26071  fvray  26080  fvline  26083  linerflx1  26088  ellines  26091  ftc1anc  26302  ivthALT  26352  sdclem1  26461  sstotbnd2  26497  zerdivemp1x  26585  isdrngo2  26588  iscringd  26623  irrapxlem6  26904  jm2.26lem3  27086  dgrsub2  27330  mpaadgr  27350  pmtrprfv  27387  psgnunilem3  27410  matrng  27471  matassa  27472  mendrng  27491  mendlmod  27492  mendassa  27493  fmuldfeq  27703  stoweidlem43  27782  stoweidlem52  27791  stoweidlem53  27792  stoweidlem56  27795  stoweidlem57  27796  elfzelfzelfz  28132  swdeq  28230  2cshw1lem2  28283  2cshw2lem2  28287  2cshw2lem3  28288  el2spthonot0  28403  el2wlkonotot0  28404  usg2wotspth  28416  2pthwlkonot  28417  bnj149  29320  bnj1118  29427  bnj1128  29433  lsmsat  29880  lfladdcl  29943  lflnegcl  29947  lflvscl  29949  lshpkrlem4  29985  lshpkrlem6  29987  ldualgrplem  30017  lduallmodlem  30024  latmassOLD  30101  latm12  30102  latm32  30103  latmrot  30104  latmmdiN  30106  latmmdir  30107  omlfh1N  30130  omlfh3N  30131  cvlexchb1  30202  cvlexch3  30204  cvlexch4N  30205  cvlatexchb1  30206  cvlsupr2  30215  hlatjass  30241  hlatj12  30242  hlatj32  30243  cvratlem  30292  cvrat  30293  atcvrj0  30299  cvrat2  30300  atltcvr  30306  atexchltN  30312  cvrat3  30313  cvrat4  30314  3dimlem3  30332  3dimlem3OLDN  30333  3at  30361  2atneat  30386  llncmp  30393  2at0mat0  30396  2atmat0  30397  lplnnle2at  30412  llncvrlpln  30429  lplncmp  30433  lplnexllnN  30435  2llnjaN  30437  4atlem11  30480  lplncvrlvol  30487  lvolcmp  30488  2atm2atN  30656  elpaddatriN  30674  paddasslem9  30699  paddass  30709  padd12N  30710  paddssw2  30715  paddss  30716  pmodlem2  30718  pmodN  30721  pmapjlln1  30726  atmod1i1  30728  atmod1i2  30730  pexmidlem2N  30842  pexmidlem6N  30846  pl42N  30854  lhpm0atN  30900  lautlt  30962  lautcvr  30963  lautj  30964  lautm  30965  ltrneq2  31019  cdlemc3  31064  cdlemc4  31065  cdlemd1  31069  cdleme1b  31097  cdleme1  31098  cdleme2  31099  cdleme3e  31103  cdlemefr27cl  31274  cdlemefs27cl  31284  cdleme42mN  31358  cdlemftr2  31437  trljco  31611  tgrpgrplem  31620  tendoplass  31654  tendodi1  31655  tendodi2  31656  cdlemk36  31784  erngdvlem3  31861  erngdvlem3-rN  31869  tendospdi1  31892  dvalveclem  31897  dialss  31918  dvhvaddass  31969  dvhopvsca  31974  dvhlveclem  31980  diblss  32042  diclss  32065  dihmeetlem12N  32190  dihmeetlem15N  32193  dihmeetlem16N  32194  dihmeetlem17N  32195  dihmeetlem18N  32196  dihmeetlem19N  32197  dvh4dimN  32319  lpolvN  32358  lclkr  32405  lclkrs  32411  lcfr  32457
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator