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  4653  isopolem  5929  frfi  7192  intrnfi  7260  iinfi  7261  eqsup  7297  fisupcl  7308  cnfcomlem  7492  ackbij1lem15  7950  fpwwe2lem5  8346  ico0  10794  elioc2  10805  elico2  10806  elicc2  10807  iccsplit  10860  fseq1p1m1  10949  ccatswrd  11555  tanadd  12544  dvds2ln  12656  qredeq  12882  ressress  13302  mreexexlem4d  13648  mreexexd  13649  0catg  13688  2oppccomf  13727  issubc3  13822  fthmon  13900  fuccocl  13937  fucidcl  13938  invfuc  13947  curf2cl  14104  yonedalem4c  14150  yonedalem3  14153  pospo  14206  latjlej1  14270  latnlej2  14276  latmlem1  14286  latledi  14294  latmlej11  14295  latjass  14300  latj12  14301  latj32  14302  latj13  14303  latj31  14304  latjrot  14305  latjjdi  14308  latjjdir  14309  latdisdlem  14391  prdsmndd  14504  imasmnd2  14508  frmdmnd  14580  grpsubrcan  14646  grpsubadd  14652  grpsubsub  14653  grpaddsubass  14654  grpsubsub4  14657  grpnnncan2  14660  mulgnndir  14688  mulgnn0dir  14689  mulgdir  14691  mulgnnass  14694  mulgnn0ass  14695  mulgass  14696  mulgsubdir  14697  pwsmulg  14708  imasgrp2  14709  issubg2  14735  eqgval  14765  divsgrp  14771  galcan  14857  gacan  14858  symggrp  14879  oppgmnd  14926  cmn32  15206  cmn12  15208  abladdsub  15215  mulgnn0di  15224  mulgdi  15225  mulgsubdi  15228  dprdss  15363  dprdz  15364  dprdf1o  15366  dprdsn  15370  dprd2da  15376  ablfac1b  15404  pgpfac1lem5  15413  rngi  15452  prdsrngd  15494  imasrng  15501  opprrng  15512  mulgass3  15518  dvrass  15571  subrgunit  15662  issubrg2  15664  abvdiv  15701  islss3  15815  prdslmodd  15825  islmhm2  15894  lspsolv  15995  islbs2  16006  islbs3  16007  lbsextlem4  16013  sralmod  16038  issubassa  16163  sraassa  16164  psrbaglecl  16214  psrbagcon  16216  psrgrp  16242  psrlmod  16245  psrrng  16254  psrassa  16257  ipdir  16649  ipdi  16650  ipsubdir  16652  ipsubdi  16653  ipass  16655  ipassr  16656  ipassr2  16657  ocvlss  16678  iinopn  16754  subbascn  17090  nrmsep2  17190  isnrm3  17193  regsep2  17210  dnsconst  17212  dfcon2  17251  1stcelcls  17293  nllyidm  17321  dislly  17329  upxp  17423  fbasne0  17627  filss  17650  infil  17660  fsubbas  17664  filssufilg  17708  tmdcn2  17874  isxmet2d  17994  xmettri  18017  xmetres2  18027  bldisj  18057  blss2  18061  xmstri2  18114  mstri2  18115  xmstri  18116  mstri  18117  xmstri3  18118  mstri3  18119  msrtri  18120  comet  18161  stdbdbl  18165  met2ndci  18170  ngprcan  18233  ngplcan  18234  ngpsubcan  18237  nrgdsdi  18278  nrgdsdir  18279  nlmdsdi  18294  nlmdsdir  18295  blcvx  18406  icccmplem2  18431  pi1grplem  18651  pi1cof  18661  cphdivcl  18722  cphsubdir  18747  cphsubdi  18748  cphassr  18751  bcthlem5  18854  volfiniun  19008  volcn  19065  itg1val2  19143  dvconst  19370  dvlip  19444  dvfsumlem4  19480  ftc1a  19488  ulmval  19863  ulmdvlem3  19885  ang180  20223  cvxcl  20390  scvxcvx  20391  sgmmul  20552  logexprlim  20576  dchrabl  20605  grpodivdiv  21027  grpomuldivass  21028  grpopnpcan2  21032  ablodivdiv4  21070  ablonnncan  21072  ablonnncan1  21074  zerdivemp1  21213  nvmdi  21322  dipassr  21538  dvrdir  23418  dvrcan5  23421  kerf1hrm  23428  tpr2rico  23466  qqhval2lem  23638  qqhvq  23644  issiga  23760  measdivcstOLD  23842  measdivcst  23843  erdszelem9  24134  rescon  24181  cvmseu  24211  cvmlift2lem12  24249  iseupa  24285  dedekindle  24489  colinearalglem1  25093  colinearalg  25097  axcgrtr  25102  axlowdimlem16  25144  axeuclidlem  25149  axcontlem7  25157  cgrid2  25185  segconeu  25193  btwncomim  25195  btwnswapid  25199  cgrxfr  25237  btwnxfr  25238  colineardim1  25243  brofs2  25259  brifs2  25260  idinside  25266  endofsegid  25267  btwnconn1lem7  25275  btwnconn1lem11  25279  btwnconn1  25283  segcon2  25287  seglemin  25295  segletr  25296  btwnsegle  25299  colinbtwnle  25300  broutsideof2  25304  broutsideof3  25308  outsidele  25314  fvray  25323  fvline  25326  linerflx1  25331  ellines  25334  ivthALT  25582  sdclem1  25777  sstotbnd2  25821  zerdivemp1x  25909  isdrngo2  25912  iscringd  25947  irrapxlem6  26235  jm2.26lem3  26417  dgrsub2  26662  mpaadgr  26682  pmtrprfv  26719  psgnunilem3  26742  matrng  26803  matassa  26804  mendrng  26823  mendlmod  26824  mendassa  26825  fmuldfeq  27036  stoweidlem43  27115  stoweidlem53  27125  stoweidlem56  27128  stoweidlem57  27129  hashtpg  27471  wlkoniswlk  27685  constr2trl  27734  wlkdvspth  27744  bnj149  28669  bnj1118  28776  bnj1128  28782  lsmsat  29267  lfladdcl  29330  lflnegcl  29334  lflvscl  29336  lshpkrlem4  29372  lshpkrlem6  29374  ldualgrplem  29404  lduallmodlem  29411  latmassOLD  29488  latm12  29489  latm32  29490  latmrot  29491  latmmdiN  29493  latmmdir  29494  omlfh1N  29517  omlfh3N  29518  cvlexchb1  29589  cvlexch3  29591  cvlexch4N  29592  cvlatexchb1  29593  cvlsupr2  29602  hlatjass  29628  hlatj12  29629  hlatj32  29630  cvratlem  29679  cvrat  29680  atcvrj0  29686  cvrat2  29687  atltcvr  29693  atexchltN  29699  cvrat3  29700  cvrat4  29701  3dimlem3  29719  3dimlem3OLDN  29720  3at  29748  2atneat  29773  llncmp  29780  2at0mat0  29783  2atmat0  29784  lplnnle2at  29799  llncvrlpln  29816  lplncmp  29820  lplnexllnN  29822  2llnjaN  29824  4atlem11  29867  lplncvrlvol  29874  lvolcmp  29875  2atm2atN  30043  elpaddatriN  30061  paddasslem9  30086  paddass  30096  padd12N  30097  paddssw2  30102  paddss  30103  pmodlem2  30105  pmodN  30108  pmapjlln1  30113  atmod1i1  30115  atmod1i2  30117  pexmidlem2N  30229  pexmidlem6N  30233  pl42N  30241  lhpm0atN  30287  lautlt  30349  lautcvr  30350  lautj  30351  lautm  30352  ltrneq2  30406  cdlemc3  30451  cdlemc4  30452  cdlemd1  30456  cdleme1b  30484  cdleme1  30485  cdleme2  30486  cdleme3e  30490  cdlemefr27cl  30661  cdlemefs27cl  30671  cdleme42mN  30745  cdlemftr2  30824  trljco  30998  tgrpgrplem  31007  tendoplass  31041  tendodi1  31042  tendodi2  31043  cdlemk36  31171  erngdvlem3  31248  erngdvlem3-rN  31256  tendospdi1  31279  dvalveclem  31284  dialss  31305  dvhvaddass  31356  dvhopvsca  31361  dvhlveclem  31367  diblss  31429  diclss  31452  dihmeetlem12N  31577  dihmeetlem15N  31580  dihmeetlem16N  31581  dihmeetlem17N  31582  dihmeetlem18N  31583  dihmeetlem19N  31584  dvh4dimN  31706  lpolvN  31745  lclkr  31792  lclkrs  31798  lcfr  31844
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