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

Theorem simpr1 963
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 957 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
21adantl 453 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  simplr1  999  simprr1  1005  simp1r1  1053  simp2r1  1059  simp3r1  1065  3anandis  1285  fr3nr  4719  isopolem  6024  frfi  7311  intrnfi  7379  iinfi  7380  eqsup  7417  fisupcl  7428  cnfcomlem  7612  ackbij1lem15  8070  fpwwe2lem5  8465  ico0  10918  elioc2  10929  elico2  10930  elicc2  10931  iccsplit  10985  fseq1p1m1  11077  hashtpg  11646  ccatswrd  11728  tanadd  12723  dvds2ln  12835  qredeq  13061  ressress  13481  mreexexlem4d  13827  mreexexd  13828  0catg  13867  2oppccomf  13906  issubc3  14001  fthmon  14079  fuccocl  14116  fucidcl  14117  invfuc  14126  curf2cl  14283  yonedalem4c  14329  yonedalem3  14332  pospo  14385  latjlej1  14449  latnlej2  14455  latmlem1  14465  latledi  14473  latmlej11  14474  latjass  14479  latj12  14480  latj32  14481  latj13  14482  latj31  14483  latjrot  14484  latjjdi  14487  latjjdir  14488  latdisdlem  14570  prdsmndd  14683  imasmnd2  14687  frmdmnd  14759  grpsubrcan  14825  grpsubadd  14831  grpsubsub  14832  grpaddsubass  14833  grpsubsub4  14836  grpnnncan2  14839  mulgnndir  14867  mulgnn0dir  14868  mulgdir  14870  mulgnnass  14873  mulgnn0ass  14874  mulgass  14875  mulgsubdir  14876  pwsmulg  14887  imasgrp2  14888  issubg2  14914  eqgval  14944  divsgrp  14950  galcan  15036  gacan  15037  symggrp  15058  oppgmnd  15105  cmn32  15385  cmn12  15387  abladdsub  15394  mulgnn0di  15403  mulgdi  15404  mulgsubdi  15407  dprdss  15542  dprdz  15543  dprdf1o  15545  dprdsn  15549  dprd2da  15555  ablfac1b  15583  pgpfac1lem5  15592  rngi  15631  prdsrngd  15673  imasrng  15680  opprrng  15691  mulgass3  15697  dvrass  15750  subrgunit  15841  issubrg2  15843  abvdiv  15880  islss3  15990  prdslmodd  16000  islmhm2  16069  lspsolv  16170  islbs2  16181  islbs3  16182  lbsextlem4  16188  sralmod  16213  issubassa  16338  sraassa  16339  psrbaglecl  16389  psrbagcon  16391  psrgrp  16417  psrlmod  16420  psrrng  16429  psrassa  16432  ipdir  16825  ipdi  16826  ipsubdir  16828  ipsubdi  16829  ipass  16831  ipassr  16832  ipassr2  16833  ocvlss  16854  iinopn  16930  subbascn  17272  nrmsep2  17374  isnrm3  17377  regsep2  17394  dnsconst  17396  dfcon2  17435  1stcelcls  17477  nllyidm  17505  dislly  17513  upxp  17608  fbasne0  17815  filss  17838  infil  17848  fsubbas  17852  filssufilg  17896  tmdcn2  18072  psmettri  18295  isxmet2d  18310  xmettri  18334  xmetres2  18344  bldisj  18381  blss2ps  18386  blss2  18387  xmstri2  18449  mstri2  18450  xmstri  18451  mstri  18452  xmstri3  18453  mstri3  18454  msrtri  18455  comet  18496  stdbdbl  18500  met2ndci  18505  ngprcan  18609  ngplcan  18610  ngpsubcan  18613  nrgdsdi  18654  nrgdsdir  18655  nlmdsdi  18670  nlmdsdir  18671  blcvx  18782  icccmplem2  18807  pi1grplem  19027  pi1cof  19037  cphdivcl  19098  cphsubdir  19123  cphsubdi  19124  cphassr  19127  bcthlem5  19234  volfiniun  19394  volcn  19451  itg1val2  19529  dvconst  19756  dvlip  19830  dvfsumlem4  19866  ftc1a  19874  ulmval  20249  ulmdvlem3  20271  ang180  20609  cvxcl  20776  scvxcvx  20777  sgmmul  20938  logexprlim  20962  dchrabl  20991  wlkoniswlk  21486  constr2trl  21552  wlkdvspth  21561  iseupa  21640  grpodivdiv  21789  grpomuldivass  21790  grpopnpcan2  21794  ablodivdiv4  21832  ablonnncan  21834  ablonnncan1  21836  zerdivemp1  21975  nvmdi  22084  dipassr  22300  dvrdir  24179  dvrcan5  24182  kerf1hrm  24215  reofld  24233  pstmfval  24244  tpr2rico  24263  qqhval2lem  24318  qqhvq  24324  issiga  24447  measdivcstOLD  24531  measdivcst  24532  erdszelem9  24838  rescon  24886  cvmseu  24916  cvmlift2lem12  24954  dedekindle  25141  colinearalglem1  25749  colinearalg  25753  axcgrtr  25758  axlowdimlem16  25800  axeuclidlem  25805  axcontlem7  25813  cgrid2  25841  segconeu  25849  btwncomim  25851  btwnswapid  25855  cgrxfr  25893  btwnxfr  25894  colineardim1  25899  brofs2  25915  brifs2  25916  idinside  25922  endofsegid  25923  btwnconn1lem7  25931  btwnconn1lem11  25935  btwnconn1  25939  segcon2  25943  seglemin  25951  segletr  25952  btwnsegle  25955  colinbtwnle  25956  broutsideof2  25960  broutsideof3  25964  outsidele  25970  fvray  25979  fvline  25982  linerflx1  25987  ellines  25990  ivthALT  26228  sdclem1  26337  sstotbnd2  26373  zerdivemp1x  26461  isdrngo2  26464  iscringd  26499  irrapxlem6  26780  jm2.26lem3  26962  dgrsub2  27207  mpaadgr  27227  pmtrprfv  27264  psgnunilem3  27287  matrng  27348  matassa  27349  mendrng  27368  mendlmod  27369  mendassa  27370  fmuldfeq  27580  stoweidlem43  27659  stoweidlem52  27668  stoweidlem53  27669  stoweidlem56  27672  stoweidlem57  27673  elfzelfzelfz  27981  el2spthonot0  28068  el2wlkonotot0  28069  usg2wotspth  28081  2pthwlkonot  28082  bnj149  28952  bnj1118  29059  bnj1128  29065  lsmsat  29491  lfladdcl  29554  lflnegcl  29558  lflvscl  29560  lshpkrlem4  29596  lshpkrlem6  29598  ldualgrplem  29628  lduallmodlem  29635  latmassOLD  29712  latm12  29713  latm32  29714  latmrot  29715  latmmdiN  29717  latmmdir  29718  omlfh1N  29741  omlfh3N  29742  cvlexchb1  29813  cvlexch3  29815  cvlexch4N  29816  cvlatexchb1  29817  cvlsupr2  29826  hlatjass  29852  hlatj12  29853  hlatj32  29854  cvratlem  29903  cvrat  29904  atcvrj0  29910  cvrat2  29911  atltcvr  29917  atexchltN  29923  cvrat3  29924  cvrat4  29925  3dimlem3  29943  3dimlem3OLDN  29944  3at  29972  2atneat  29997  llncmp  30004  2at0mat0  30007  2atmat0  30008  lplnnle2at  30023  llncvrlpln  30040  lplncmp  30044  lplnexllnN  30046  2llnjaN  30048  4atlem11  30091  lplncvrlvol  30098  lvolcmp  30099  2atm2atN  30267  elpaddatriN  30285  paddasslem9  30310  paddass  30320  padd12N  30321  paddssw2  30326  paddss  30327  pmodlem2  30329  pmodN  30332  pmapjlln1  30337  atmod1i1  30339  atmod1i2  30341  pexmidlem2N  30453  pexmidlem6N  30457  pl42N  30465  lhpm0atN  30511  lautlt  30573  lautcvr  30574  lautj  30575  lautm  30576  ltrneq2  30630  cdlemc3  30675  cdlemc4  30676  cdlemd1  30680  cdleme1b  30708  cdleme1  30709  cdleme2  30710  cdleme3e  30714  cdlemefr27cl  30885  cdlemefs27cl  30895  cdleme42mN  30969  cdlemftr2  31048  trljco  31222  tgrpgrplem  31231  tendoplass  31265  tendodi1  31266  tendodi2  31267  cdlemk36  31395  erngdvlem3  31472  erngdvlem3-rN  31480  tendospdi1  31503  dvalveclem  31508  dialss  31529  dvhvaddass  31580  dvhopvsca  31585  dvhlveclem  31591  diblss  31653  diclss  31676  dihmeetlem12N  31801  dihmeetlem15N  31804  dihmeetlem16N  31805  dihmeetlem17N  31806  dihmeetlem18N  31807  dihmeetlem19N  31808  dvh4dimN  31930  lpolvN  31969  lclkr  32016  lclkrs  32022  lcfr  32068
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator