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  4727  isopolem  6032  frfi  7319  intrnfi  7387  iinfi  7388  eqsup  7425  fisupcl  7436  cnfcomlem  7620  ackbij1lem15  8078  fpwwe2lem5  8473  ico0  10926  elioc2  10937  elico2  10938  elicc2  10939  iccsplit  10993  fseq1p1m1  11085  hashtpg  11654  ccatswrd  11736  tanadd  12731  dvds2ln  12843  qredeq  13069  ressress  13489  mreexexlem4d  13835  mreexexd  13836  0catg  13875  2oppccomf  13914  issubc3  14009  fthmon  14087  fuccocl  14124  fucidcl  14125  invfuc  14134  curf2cl  14291  yonedalem4c  14337  yonedalem3  14340  pospo  14393  latjlej1  14457  latnlej2  14463  latmlem1  14473  latledi  14481  latmlej11  14482  latjass  14487  latj12  14488  latj32  14489  latj13  14490  latj31  14491  latjrot  14492  latjjdi  14495  latjjdir  14496  latdisdlem  14578  prdsmndd  14691  imasmnd2  14695  frmdmnd  14767  grpsubrcan  14833  grpsubadd  14839  grpsubsub  14840  grpaddsubass  14841  grpsubsub4  14844  grpnnncan2  14847  mulgnndir  14875  mulgnn0dir  14876  mulgdir  14878  mulgnnass  14881  mulgnn0ass  14882  mulgass  14883  mulgsubdir  14884  pwsmulg  14895  imasgrp2  14896  issubg2  14922  eqgval  14952  divsgrp  14958  galcan  15044  gacan  15045  symggrp  15066  oppgmnd  15113  cmn32  15393  cmn12  15395  abladdsub  15402  mulgnn0di  15411  mulgdi  15412  mulgsubdi  15415  dprdss  15550  dprdz  15551  dprdf1o  15553  dprdsn  15557  dprd2da  15563  ablfac1b  15591  pgpfac1lem5  15600  rngi  15639  prdsrngd  15681  imasrng  15688  opprrng  15699  mulgass3  15705  dvrass  15758  subrgunit  15849  issubrg2  15851  abvdiv  15888  islss3  15998  prdslmodd  16008  islmhm2  16077  lspsolv  16178  islbs2  16189  islbs3  16190  lbsextlem4  16196  sralmod  16221  issubassa  16346  sraassa  16347  psrbaglecl  16397  psrbagcon  16399  psrgrp  16425  psrlmod  16428  psrrng  16437  psrassa  16440  ipdir  16833  ipdi  16834  ipsubdir  16836  ipsubdi  16837  ipass  16839  ipassr  16840  ipassr2  16841  ocvlss  16862  iinopn  16938  subbascn  17280  nrmsep2  17382  isnrm3  17385  regsep2  17402  dnsconst  17404  dfcon2  17443  1stcelcls  17485  nllyidm  17513  dislly  17521  upxp  17616  fbasne0  17823  filss  17846  infil  17856  fsubbas  17860  filssufilg  17904  tmdcn2  18080  psmettri  18303  isxmet2d  18318  xmettri  18342  xmetres2  18352  bldisj  18389  blss2ps  18394  blss2  18395  xmstri2  18457  mstri2  18458  xmstri  18459  mstri  18460  xmstri3  18461  mstri3  18462  msrtri  18463  comet  18504  stdbdbl  18508  met2ndci  18513  ngprcan  18617  ngplcan  18618  ngpsubcan  18621  nrgdsdi  18662  nrgdsdir  18663  nlmdsdi  18678  nlmdsdir  18679  blcvx  18790  icccmplem2  18815  pi1grplem  19035  pi1cof  19045  cphdivcl  19106  cphsubdir  19131  cphsubdi  19132  cphassr  19135  bcthlem5  19242  volfiniun  19402  volcn  19459  itg1val2  19537  dvconst  19764  dvlip  19838  dvfsumlem4  19874  ftc1a  19882  ulmval  20257  ulmdvlem3  20279  ang180  20617  cvxcl  20784  scvxcvx  20785  sgmmul  20946  logexprlim  20970  dchrabl  20999  wlkoniswlk  21494  constr2trl  21560  wlkdvspth  21569  iseupa  21648  grpodivdiv  21797  grpomuldivass  21798  grpopnpcan2  21802  ablodivdiv4  21840  ablonnncan  21842  ablonnncan1  21844  zerdivemp1  21983  nvmdi  22092  dipassr  22308  dvrdir  24187  dvrcan5  24190  kerf1hrm  24223  reofld  24241  pstmfval  24252  tpr2rico  24271  qqhval2lem  24326  qqhvq  24332  issiga  24455  measdivcstOLD  24539  measdivcst  24540  erdszelem9  24846  rescon  24894  cvmseu  24924  cvmlift2lem12  24962  dedekindle  25149  colinearalglem1  25757  colinearalg  25761  axcgrtr  25766  axlowdimlem16  25808  axeuclidlem  25813  axcontlem7  25821  cgrid2  25849  segconeu  25857  btwncomim  25859  btwnswapid  25863  cgrxfr  25901  btwnxfr  25902  colineardim1  25907  brofs2  25923  brifs2  25924  idinside  25930  endofsegid  25931  btwnconn1lem7  25939  btwnconn1lem11  25943  btwnconn1  25947  segcon2  25951  seglemin  25959  segletr  25960  btwnsegle  25963  colinbtwnle  25964  broutsideof2  25968  broutsideof3  25972  outsidele  25978  fvray  25987  fvline  25990  linerflx1  25995  ellines  25998  ivthALT  26236  sdclem1  26345  sstotbnd2  26381  zerdivemp1x  26469  isdrngo2  26472  iscringd  26507  irrapxlem6  26788  jm2.26lem3  26970  dgrsub2  27215  mpaadgr  27235  pmtrprfv  27272  psgnunilem3  27295  matrng  27356  matassa  27357  mendrng  27376  mendlmod  27377  mendassa  27378  fmuldfeq  27588  stoweidlem43  27667  stoweidlem52  27676  stoweidlem53  27677  stoweidlem56  27680  stoweidlem57  27681  elfzelfzelfz  27989  el2spthonot0  28076  el2wlkonotot0  28077  usg2wotspth  28089  2pthwlkonot  28090  bnj149  28964  bnj1118  29071  bnj1128  29077  lsmsat  29503  lfladdcl  29566  lflnegcl  29570  lflvscl  29572  lshpkrlem4  29608  lshpkrlem6  29610  ldualgrplem  29640  lduallmodlem  29647  latmassOLD  29724  latm12  29725  latm32  29726  latmrot  29727  latmmdiN  29729  latmmdir  29730  omlfh1N  29753  omlfh3N  29754  cvlexchb1  29825  cvlexch3  29827  cvlexch4N  29828  cvlatexchb1  29829  cvlsupr2  29838  hlatjass  29864  hlatj12  29865  hlatj32  29866  cvratlem  29915  cvrat  29916  atcvrj0  29922  cvrat2  29923  atltcvr  29929  atexchltN  29935  cvrat3  29936  cvrat4  29937  3dimlem3  29955  3dimlem3OLDN  29956  3at  29984  2atneat  30009  llncmp  30016  2at0mat0  30019  2atmat0  30020  lplnnle2at  30035  llncvrlpln  30052  lplncmp  30056  lplnexllnN  30058  2llnjaN  30060  4atlem11  30103  lplncvrlvol  30110  lvolcmp  30111  2atm2atN  30279  elpaddatriN  30297  paddasslem9  30322  paddass  30332  padd12N  30333  paddssw2  30338  paddss  30339  pmodlem2  30341  pmodN  30344  pmapjlln1  30349  atmod1i1  30351  atmod1i2  30353  pexmidlem2N  30465  pexmidlem6N  30469  pl42N  30477  lhpm0atN  30523  lautlt  30585  lautcvr  30586  lautj  30587  lautm  30588  ltrneq2  30642  cdlemc3  30687  cdlemc4  30688  cdlemd1  30692  cdleme1b  30720  cdleme1  30721  cdleme2  30722  cdleme3e  30726  cdlemefr27cl  30897  cdlemefs27cl  30907  cdleme42mN  30981  cdlemftr2  31060  trljco  31234  tgrpgrplem  31243  tendoplass  31277  tendodi1  31278  tendodi2  31279  cdlemk36  31407  erngdvlem3  31484  erngdvlem3-rN  31492  tendospdi1  31515  dvalveclem  31520  dialss  31541  dvhvaddass  31592  dvhopvsca  31597  dvhlveclem  31603  diblss  31665  diclss  31688  dihmeetlem12N  31813  dihmeetlem15N  31816  dihmeetlem16N  31817  dihmeetlem17N  31818  dihmeetlem18N  31819  dihmeetlem19N  31820  dvh4dimN  31942  lpolvN  31981  lclkr  32028  lclkrs  32034  lcfr  32080
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