Theorem simplr 528

Description: Simplification of a conjunction. (Contributed by NM, 20-Mar-2007.)

Assertion

Ref	Expression
simplr	|- ( ( ( ph /\ ps ) /\ ch ) -> ps )

Proof of Theorem simplr

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ps -> ps )
2	1	ad2antlr 489	1 |- ( ( ( ph /\ ps ) /\ ch ) -> ps )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  simp1lr  1063  simp2lr  1067  simp3lr  1071  bilukdc  1415  dcun  3569  ifnefals  3613  intab  3913  exmid01  4241  exmidundif  4249  exmidundifim  4250  frirrg  4396  reg2exmidlema  4581  imadiflem  5352  fvco4  5650  fvmptt  5670  fcoconst  5750  funopsn  5761  f1imass  5842  fcof1  5851  fliftfun  5864  riotass2  5925  ovmpodxf  6070  dftpos4  6348  tfrlem1  6393  tfrlem3ag  6394  tfrlemibacc  6411  tfrlemibfn  6413  tfrlemi1  6417  tfrlemi14d  6418  tfr1onlem3ag  6422  tfr1onlembacc  6427  tfr1onlembfn  6429  tfr1onlemaccex  6433  tfrcllembacc  6440  tfrcllembfn  6442  tfrcllemaccex  6446  frecabcl  6484  nntr2  6588  dcdifsnid  6589  nnm00  6615  ecopovsymg  6720  ecopoverg  6722  th3qlem1  6723  mapss  6777  f1imaen2g  6884  pw2f1odclem  6930  xpen  6941  xpmapenlem  6945  phpm  6961  fidifsnen  6966  dif1enen  6976  fiunsnnn  6977  fin0  6981  fin0or  6982  findcard2d  6987  findcard2sd  6988  diffifi  6990  isinfinf  6993  tridc  6995  fimax2gtrilemstep  6996  fimax2gtri  6997  en2eqpr  7003  onunsnss  7013  unsnfidcex  7016  unsnfidcel  7017  undifdcss  7019  unfiin  7022  fisseneq  7030  ssfirab  7032  f1finf1o  7048  fidcenumlemrks  7054  fidcenumlemrk  7055  fidcenumlemr  7056  fidcenum  7057  suplub2ti  7102  supisolem  7109  ordiso2  7136  djudom  7194  omp1eomlem  7195  difinfsnlem  7200  difinfinf  7202  ctm  7210  ctssdclemn0  7211  enumct  7216  nnnninfeq  7229  nnnninfeq2  7230  nninfisol  7234  enomnilem  7239  finomni  7241  exmidomni  7243  fodju0  7248  ismkvnex  7256  enmkvlem  7262  enwomnilem  7270  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  exmidaclem  7319  exmidontriimlem1  7332  exmidontriimlem2  7333  exmidontriimlem3  7334  exmidontriimlem4  7335  exmidontriim  7336  netap  7365  exmidapne  7371  dfplpq2  7466  dfmpq2  7467  mulpipqqs  7485  nqpi  7490  distrnqg  7499  prarloclemarch  7530  enq0tr  7546  nqnq0pi  7550  nq0nn  7554  nnnq0lem1  7558  prarloclemup  7607  prarloclem3  7609  prarloclemcalc  7614  genplt2i  7622  addnqprllem  7639  addnqprulem  7640  appdivnq  7675  distrlem1prl  7694  distrlem1pru  7695  ltaddpr  7709  ltexprlemlol  7714  ltexprlemupu  7716  ltexprlemdisj  7718  addcanprleml  7726  ltaprlem  7730  addextpr  7733  recexprlemopu  7739  recexprlemdisj  7742  recexprlem1ssl  7745  aptiprleml  7751  cauappcvgprlemm  7757  cauappcvgprlemopl  7758  cauappcvgprlemlol  7759  cauappcvgprlemopu  7760  cauappcvgprlemdisj  7763  cauappcvgprlemladdfu  7766  cauappcvgprlemladdfl  7767  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  caucvgprlemm  7780  caucvgprlemopl  7781  caucvgprlemlol  7782  caucvgprlemopu  7783  caucvgprlemladdfu  7789  caucvgprprlemml  7806  caucvgprprlemopl  7809  caucvgprprlemlol  7810  caucvgprprlemopu  7811  caucvgprprlemexbt  7818  suplocexprlemru  7831  suplocexprlemloc  7833  suplocexprlemub  7835  suplocexprlemlub  7836  prsrlem1  7854  recexgt0sr  7885  mulgt0sr  7890  archsr  7894  caucvgsrlemcau  7905  caucvgsrlemoffcau  7910  caucvgsrlemoffres  7912  suplocsrlemb  7918  suplocsrlempr  7919  suplocsrlem  7920  addcnsr  7946  mulcnsr  7947  mulcnsrec  7955  axmulcom  7983  nntopi  8006  axcaucvglemcau  8010  axcaucvglemres  8011  axpre-suploclemres  8013  axpre-suploc  8014  mpomulf  8061  axsuploc  8144  ltntri  8199  cnegexlem2  8247  cnegexlem3  8248  addsub4  8314  le2add  8516  lt2add  8517  lt2sub  8532  le2sub  8533  rereim  8658  apreim  8675  mulreim  8676  apcotr  8679  apadd1  8680  addext  8682  mulext1  8684  mulext  8686  apti  8694  aptap  8722  receuap  8741  rec11rap  8783  divdivdivap  8785  divadddivap  8799  divsubdivap  8800  rerecclap  8802  recgt0  8922  prodgt0gt0  8923  prodgt0  8924  prodge0  8926  lemulge11  8938  lt2mul2div  8951  ltrec  8955  lerec  8956  ltrec1  8960  lediv2a  8967  mulle0r  9016  sup3exmid  9029  zdiv  9460  eluzuzle  9655  supinfneg  9715  infsupneg  9716  infregelbex  9718  xrltso  9917  xnn0dcle  9923  xnn0letri  9924  npnflt  9936  nmnfgt  9939  z2ge  9947  xaddf  9965  xaddval  9966  xpncan  9992  xleadd1a  9994  xltadd1  9997  xaddge0  9999  xle2add  10000  xleaddadd  10008  ixxss1  10025  ixxss2  10026  elico2  10058  iccsupr  10087  fzass4  10183  fzrev  10205  fz0fzelfz0  10248  fzocatel  10326  elfzomelpfzo  10358  zsupcllemstep  10370  exbtwnzlemstep  10388  rebtwn2zlemstep  10393  qbtwnxr  10398  xqltnle  10408  apbtwnz  10415  btwnzge0  10441  modqid  10492  modqcyc  10502  modqcyc2  10503  modqaddabs  10505  modqaddmod  10506  mulqaddmodid  10507  modqmuladd  10509  modqltm1p1mod  10519  modqsubmod  10525  modqsubmodmod  10526  modaddmodlo  10531  modqmulmod  10532  modqmulmodr  10533  modqsubdir  10536  addmodlteq  10541  nninfinf  10586  iseqf1olemab  10645  iseqf1olemmo  10648  iseqf1olemjpcl  10651  iseqf1olemqpcl  10652  seqf1oglem1  10662  seqf1oglem2  10663  seqf1og  10664  exp3val  10684  expcl2lemap  10694  expap0  10712  expnegzap  10716  expmul  10727  leexp1a  10737  qsqeqor  10793  expnbnd  10806  nn0ltexp2  10852  nn0opth2  10867  facndiv  10882  faclbnd  10884  bcval5  10906  bcpasc  10909  hashennnuni  10922  hashunlem  10947  hashunsng  10950  hashprg  10951  fiprsshashgt1  10960  hashxp  10969  fimaxq  10970  zfz1isolemiso  10982  zfz1isolem1  10983  seq3coll  10985  iswrdiz  10999  wrdnval  11022  ccatlen  11049  ccatvalfn  11055  ccatsymb  11056  shftlem  11098  shftfvalg  11100  shftfval  11103  2shfti  11113  caucvgrelemrec  11261  caucvgrelemcau  11262  caucvgre  11263  cvg1nlemcau  11266  cvg1nlemres  11267  resqrexlemcalc3  11298  resqrexlemcvg  11301  resqrexlemglsq  11304  resqrexlemga  11305  sqrtsq  11326  leabs  11356  absexpzap  11362  abslt  11370  absle  11371  abssubap0  11372  caubnd2  11399  icodiamlt  11462  maxleim  11487  maxabslemval  11490  maxleastlt  11497  rexico  11503  zmaxcl  11506  fimaxre2  11509  minmax  11512  xrmaxleim  11526  xrmaxiflemcl  11527  xrmaxifle  11528  xrmaxiflemlub  11530  xrmaxiflemval  11532  xrmaxleastlt  11538  xrmaxltsup  11540  xrmaxadd  11543  xrminmax  11547  xrbdtri  11558  climuni  11575  climshftlemg  11584  iserex  11621  climcau  11629  climrecvg1n  11630  climcvg1nlem  11631  sumeq2  11641  summodclem3  11662  zsumdc  11666  isumss  11673  fisumss  11674  sumsnf  11691  fsumconst  11736  modfsummod  11740  fsum00  11744  fsumabs  11747  fsumrelem  11753  fsumiun  11759  isumsplit  11773  divcnv  11779  geo2sum  11796  geoisumr  11800  cvgratz  11814  ntrivcvgap  11830  prodeq2  11839  prodmodclem2  11859  prodmodc  11860  zproddc  11861  fprodmul  11873  prodsnf  11874  fprodcl2lem  11887  fprodconst  11902  fprodap0  11903  fprodrec  11911  fprodap0f  11918  fprodle  11922  fprodmodd  11923  tanaddap  12021  zdvdsdc  12094  dvds2ln  12106  fsumdvds  12124  dvdsle  12126  dvdsext  12137  divalglemeunn  12203  divalglemex  12204  divalglemeuneg  12205  bitsfzo  12237  bitsmod  12238  bitsinv1lem  12243  bitsinv1  12244  dvdsbnd  12248  gcdsupex  12249  gcdsupcl  12250  dvdslegcd  12256  bezoutlemnewy  12288  bezoutlemstep  12289  bezoutlemmain  12290  bezoutlemzz  12294  bezoutlembz  12296  bezoutlembi  12297  bezoutlemle  12300  dfgcd3  12302  bezout  12303  dfgcd2  12306  dvdsmulgcd  12317  bezoutr  12324  uzwodc  12329  nninfctlemfo  12332  lcmval  12356  lcmcllem  12360  lcmneg  12367  ncoprmgcdne1b  12382  isprm2lem  12409  prmind2  12413  dvdsnprmd  12418  isprm5  12435  prmdvdsexp  12441  sqrt2irr  12455  oddpwdclemxy  12462  oddpwdclemdc  12466  nonsq  12500  pceu  12589  pcmul  12595  pc2dvds  12624  pcz  12626  pcprmpw2  12627  dvdsprmpweqle  12631  pcfac  12644  qexpz  12646  prmpwdvds  12649  1arith  12661  mul4sq  12688  4sqexercise2  12693  4sqlemsdc  12694  ennnfonelemkh  12754  ennnfonelemhf1o  12755  ennnfonelemhom  12757  ennnfonelemfun  12759  ennnfonelemf1  12760  ennnfonelemim  12766  exmidunben  12768  ctiunctlemfo  12781  omiunct  12786  ssnnctlemct  12788  isstruct2r  12814  prdsval  13076  ismgm  13160  issgrp  13206  sgrppropd  13216  sgrpidmndm  13223  mndpropd  13243  issubmnd  13245  prdsidlem  13250  resmhm2b  13292  gsumwmhm  13301  isgrpinv  13357  grplmulf1o  13377  dfgrp3mlem  13401  grplactcnv  13405  pwssub  13416  mhmid  13422  mhmmnd  13423  ghmgrp  13425  mulgval  13429  mulgfng  13431  mulgnnp1  13437  mulgnn0dir  13459  mulgneg2  13463  mhmmulg  13470  grpissubg  13501  isnsg  13509  isnsg3  13514  nmzsubg  13517  ghmmhmb  13561  ghmpreima  13573  ghmnsgpreima  13576  ghmf1  13580  ghmf1o  13582  conjghm  13583  conjnmz  13586  conjnmzb  13587  ghmcmn  13634  gsumfzconst  13648  issrg  13698  srglmhm  13726  srgrmhm  13727  isring  13733  ringadd2  13760  ringlghm  13794  ringrghm  13795  oppr1g  13815  reldvdsrsrg  13825  dvdsrvald  13826  dvdsrd  13827  dvdsrex  13831  dvdsrmul1  13835  unitgrp  13849  rhmopp  13909  subrgintm  13976  subrgpropd  13986  isdomn  14002  lmodprop2d  14081  lssvacl  14098  lssvsubcl  14099  lssvscl  14108  lsslss  14114  lss1d  14116  lsspropdg  14164  expghmap  14340  mulgghm2  14341  znunit  14392  znrrg  14393  mplvalcoe  14423  mplsubgfilemcl  14432  mplsubgfileminv  14433  mplsubgfi  14434  opnssneib  14599  restbasg  14611  restopn2  14626  iscnp4  14661  cnss2  14670  cnconst2  14676  cnptopresti  14681  cnptoprest2  14683  neitx  14711  uptx  14717  txrest  14719  txdis1cn  14721  xmetres2  14822  xblss2ps  14847  blhalf  14851  blssps  14870  blss  14871  blssexps  14872  blssex  14873  blin2  14875  metequiv2  14939  bdmetval  14943  metcnp3  14954  metcnp  14955  metcn  14957  metcnpi  14958  metcnpi2  14959  txmetcnp  14961  txmetcn  14962  qtopbas  14965  tgqioo  14998  mpomulcn  15009  fsumcncntop  15010  elcncf2  15017  mulcncflem  15050  mulcncf  15051  suplociccreex  15067  limcdifap  15105  cnplimcim  15110  cnplimccntop  15113  limccnpcntop  15118  dvcj  15152  dvmptfsum  15168  dveflem  15169  ply1termlem  15185  plyaddlem1  15190  plymullem1  15191  plycolemc  15201  plycjlemc  15203  plyrecj  15206  dvply1  15208  reeff1olem  15214  eflt  15218  sin0pilem1  15224  ptolemy  15267  coseq0q4123  15277  coseq0negpitopi  15279  cos02pilt1  15294  cos11  15296  ioocosf1o  15297  rpcxpmul2  15356  cxplt  15359  cxple  15360  cxplt3  15363  apcxp2  15382  rprelogbmul  15398  rprelogbdiv  15400  dvdsppwf1o  15432  perfect  15444  lgsval  15452  lgsfcl2  15454  lgscllem  15455  lgsval2lem  15458  lgsdir2lem4  15479  lgsdir2lem5  15480  lgsdir2  15481  lgsne0  15486  gausslemma2dlem1a  15506  gausslemma2dlem1f1o  15508  2sqlem6  15568  2sqlem10  15573  2omap  15894  pwle2  15897  pwf1oexmid  15898  subctctexmid  15899  pw1nct  15902  peano4nninf  15905  nninfalllem1  15907  nninfall  15908  nninfsellemeq  15913  nninfsellemqall  15914  nnnninfex  15921  nninfnfiinf  15922  sbthom  15927  refeq  15929  isomninnlem  15931  trilpolemeq1  15941  trilpolemlt1  15942  trirec0  15945  apdiff  15949  iswomninnlem  15950  ismkvnnlem  15953  redcwlpolemeq1  15955  ltlenmkv  15971