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  1062  simp2lr  1066  simp3lr  1070  bilukdc  1406  dcun  3547  intab  3887  exmid01  4212  exmidundif  4220  exmidundifim  4221  frirrg  4364  reg2exmidlema  4547  imadiflem  5309  fvco4  5603  fvmptt  5622  fcoconst  5702  f1imass  5790  fcof1  5799  fliftfun  5812  riotass2  5872  ovmpodxf  6016  dftpos4  6281  tfrlem1  6326  tfrlem3ag  6327  tfrlemibacc  6344  tfrlemibfn  6346  tfrlemi1  6350  tfrlemi14d  6351  tfr1onlem3ag  6355  tfr1onlembacc  6360  tfr1onlembfn  6362  tfr1onlemaccex  6366  tfrcllembacc  6373  tfrcllembfn  6375  tfrcllemaccex  6379  frecabcl  6417  nntr2  6521  dcdifsnid  6522  nnm00  6548  ecopovsymg  6651  ecopoverg  6653  th3qlem1  6654  mapss  6708  f1imaen2g  6810  xpen  6862  xpmapenlem  6866  phpm  6882  fidifsnen  6887  dif1enen  6897  fiunsnnn  6898  fin0  6902  fin0or  6903  findcard2d  6908  findcard2sd  6909  diffifi  6911  isinfinf  6914  tridc  6916  fimax2gtrilemstep  6917  fimax2gtri  6918  en2eqpr  6924  onunsnss  6933  unsnfidcex  6936  unsnfidcel  6937  undifdcss  6939  unfiin  6942  fisseneq  6948  ssfirab  6950  f1finf1o  6963  fidcenumlemrks  6969  fidcenumlemrk  6970  fidcenumlemr  6971  fidcenum  6972  suplub2ti  7017  supisolem  7024  ordiso2  7051  djudom  7109  omp1eomlem  7110  difinfsnlem  7115  difinfinf  7117  ctm  7125  ctssdclemn0  7126  enumct  7131  nnnninfeq  7143  nnnninfeq2  7144  nninfisol  7148  enomnilem  7153  finomni  7155  exmidomni  7157  fodju0  7162  ismkvnex  7170  enmkvlem  7176  enwomnilem  7184  exmidfodomrlemr  7218  exmidfodomrlemrALT  7219  exmidaclem  7224  exmidontriimlem1  7237  exmidontriimlem2  7238  exmidontriimlem3  7239  exmidontriimlem4  7240  exmidontriim  7241  netap  7270  exmidapne  7276  dfplpq2  7370  dfmpq2  7371  mulpipqqs  7389  nqpi  7394  distrnqg  7403  prarloclemarch  7434  enq0tr  7450  nqnq0pi  7454  nq0nn  7458  nnnq0lem1  7462  prarloclemup  7511  prarloclem3  7513  prarloclemcalc  7518  genplt2i  7526  addnqprllem  7543  addnqprulem  7544  appdivnq  7579  distrlem1prl  7598  distrlem1pru  7599  ltaddpr  7613  ltexprlemlol  7618  ltexprlemupu  7620  ltexprlemdisj  7622  addcanprleml  7630  ltaprlem  7634  addextpr  7637  recexprlemopu  7643  recexprlemdisj  7646  recexprlem1ssl  7649  aptiprleml  7655  cauappcvgprlemm  7661  cauappcvgprlemopl  7662  cauappcvgprlemlol  7663  cauappcvgprlemopu  7664  cauappcvgprlemdisj  7667  cauappcvgprlemladdfu  7670  cauappcvgprlemladdfl  7671  cauappcvgprlemladdru  7672  cauappcvgprlemladdrl  7673  caucvgprlemm  7684  caucvgprlemopl  7685  caucvgprlemlol  7686  caucvgprlemopu  7687  caucvgprlemladdfu  7693  caucvgprprlemml  7710  caucvgprprlemopl  7713  caucvgprprlemlol  7714  caucvgprprlemopu  7715  caucvgprprlemexbt  7722  suplocexprlemru  7735  suplocexprlemloc  7737  suplocexprlemub  7739  suplocexprlemlub  7740  prsrlem1  7758  recexgt0sr  7789  mulgt0sr  7794  archsr  7798  caucvgsrlemcau  7809  caucvgsrlemoffcau  7814  caucvgsrlemoffres  7816  suplocsrlemb  7822  suplocsrlempr  7823  suplocsrlem  7824  addcnsr  7850  mulcnsr  7851  mulcnsrec  7859  axmulcom  7887  nntopi  7910  axcaucvglemcau  7914  axcaucvglemres  7915  axpre-suploclemres  7917  axpre-suploc  7918  axsuploc  8047  ltntri  8102  cnegexlem2  8150  cnegexlem3  8151  addsub4  8217  le2add  8418  lt2add  8419  lt2sub  8434  le2sub  8435  rereim  8560  apreim  8577  mulreim  8578  apcotr  8581  apadd1  8582  addext  8584  mulext1  8586  mulext  8588  apti  8596  aptap  8624  receuap  8643  rec11rap  8685  divdivdivap  8687  divadddivap  8701  divsubdivap  8702  rerecclap  8704  recgt0  8824  prodgt0gt0  8825  prodgt0  8826  prodge0  8828  lemulge11  8840  lt2mul2div  8853  ltrec  8857  lerec  8858  ltrec1  8862  lediv2a  8869  mulle0r  8918  sup3exmid  8931  zdiv  9358  eluzuzle  9553  supinfneg  9612  infsupneg  9613  infregelbex  9615  xrltso  9813  xnn0dcle  9819  xnn0letri  9820  npnflt  9832  nmnfgt  9835  z2ge  9843  xaddf  9861  xaddval  9862  xpncan  9888  xleadd1a  9890  xltadd1  9893  xaddge0  9895  xle2add  9896  xleaddadd  9904  ixxss1  9921  ixxss2  9922  elico2  9954  iccsupr  9983  fzass4  10079  fzrev  10101  fz0fzelfz0  10144  fzocatel  10216  elfzomelpfzo  10248  exbtwnzlemstep  10265  rebtwn2zlemstep  10270  qbtwnxr  10275  apbtwnz  10291  btwnzge0  10317  modqid  10366  modqcyc  10376  modqcyc2  10377  modqaddabs  10379  modqaddmod  10380  mulqaddmodid  10381  modqmuladd  10383  modqltm1p1mod  10393  modqsubmod  10399  modqsubmodmod  10400  modaddmodlo  10405  modqmulmod  10406  modqmulmodr  10407  modqsubdir  10410  addmodlteq  10415  iseqf1olemab  10506  iseqf1olemmo  10509  iseqf1olemjpcl  10512  iseqf1olemqpcl  10513  exp3val  10539  expcl2lemap  10549  expap0  10567  expnegzap  10571  expmul  10582  leexp1a  10592  qsqeqor  10648  expnbnd  10661  nn0ltexp2  10706  nn0opth2  10721  facndiv  10736  faclbnd  10738  bcval5  10760  bcpasc  10763  hashennnuni  10776  hashunlem  10801  hashunsng  10804  hashprg  10805  fiprsshashgt1  10814  hashxp  10823  fimaxq  10824  zfz1isolemiso  10836  zfz1isolem1  10837  seq3coll  10839  shftlem  10842  shftfvalg  10844  shftfval  10847  2shfti  10857  caucvgrelemrec  11005  caucvgrelemcau  11006  caucvgre  11007  cvg1nlemcau  11010  cvg1nlemres  11011  resqrexlemcalc3  11042  resqrexlemcvg  11045  resqrexlemglsq  11048  resqrexlemga  11049  sqrtsq  11070  leabs  11100  absexpzap  11106  abslt  11114  absle  11115  abssubap0  11116  caubnd2  11143  icodiamlt  11206  maxleim  11231  maxabslemval  11234  maxleastlt  11241  rexico  11247  zmaxcl  11250  fimaxre2  11252  minmax  11255  xrmaxleim  11269  xrmaxiflemcl  11270  xrmaxifle  11271  xrmaxiflemlub  11273  xrmaxiflemval  11275  xrmaxleastlt  11281  xrmaxltsup  11283  xrmaxadd  11286  xrminmax  11290  xrbdtri  11301  climuni  11318  climshftlemg  11327  iserex  11364  climcau  11372  climrecvg1n  11373  climcvg1nlem  11374  sumeq2  11384  summodclem3  11405  zsumdc  11409  isumss  11416  fisumss  11417  sumsnf  11434  fsumconst  11479  modfsummod  11483  fsum00  11487  fsumabs  11490  fsumrelem  11496  fsumiun  11502  isumsplit  11516  divcnv  11522  geo2sum  11539  geoisumr  11543  cvgratz  11557  ntrivcvgap  11573  prodeq2  11582  prodmodclem2  11602  prodmodc  11603  zproddc  11604  fprodmul  11616  prodsnf  11617  fprodcl2lem  11630  fprodconst  11645  fprodap0  11646  fprodrec  11654  fprodap0f  11661  fprodle  11665  fprodmodd  11666  tanaddap  11764  zdvdsdc  11836  dvds2ln  11848  dvdsle  11867  dvdsext  11878  divalglemeunn  11943  divalglemex  11944  divalglemeuneg  11945  zsupcllemstep  11963  dvdsbnd  11974  gcdsupex  11975  gcdsupcl  11976  dvdslegcd  11982  bezoutlemnewy  12014  bezoutlemstep  12015  bezoutlemmain  12016  bezoutlemzz  12020  bezoutlembz  12022  bezoutlembi  12023  bezoutlemle  12026  dfgcd3  12028  bezout  12029  dfgcd2  12032  dvdsmulgcd  12043  bezoutr  12050  uzwodc  12055  lcmval  12080  lcmcllem  12084  lcmneg  12091  ncoprmgcdne1b  12106  isprm2lem  12133  prmind2  12137  dvdsnprmd  12142  isprm5  12159  prmdvdsexp  12165  sqrt2irr  12179  oddpwdclemxy  12186  oddpwdclemdc  12190  nonsq  12224  pceu  12312  pcmul  12318  pc2dvds  12346  pcz  12348  pcprmpw2  12349  dvdsprmpweqle  12353  pcfac  12365  qexpz  12367  prmpwdvds  12370  1arith  12382  mul4sq  12409  ennnfonelemkh  12430  ennnfonelemhf1o  12431  ennnfonelemhom  12433  ennnfonelemfun  12435  ennnfonelemf1  12436  ennnfonelemim  12442  exmidunben  12444  ctiunctlemfo  12457  omiunct  12462  ssnnctlemct  12464  isstruct2r  12490  ismgm  12798  issgrp  12831  sgrppropd  12841  sgrpidmndm  12846  mndpropd  12866  issubmnd  12868  resmhm2b  12906  isgrpinv  12963  grplmulf1o  12983  dfgrp3mlem  13007  grplactcnv  13011  mhmid  13022  mhmmnd  13023  ghmgrp  13025  mulgval  13029  mulgfng  13031  mulgnnp1  13035  mulgnn0dir  13057  mulgneg2  13061  mhmmulg  13068  grpissubg  13098  isnsg  13106  isnsg3  13111  nmzsubg  13114  ghmmhmb  13153  ghmpreima  13165  ghmnsgpreima  13168  ghmf1  13172  ghmf1o  13174  conjghm  13175  conjnmz  13178  conjnmzb  13179  ghmcmn  13225  issrg  13279  srglmhm  13307  srgrmhm  13308  isring  13314  ringadd2  13341  oppr1g  13392  reldvdsrsrg  13402  dvdsrvald  13403  dvdsrd  13404  dvdsrex  13408  dvdsrmul1  13412  unitgrp  13426  rhmopp  13486  subrgintm  13550  subrgpropd  13555  lmodprop2d  13624  lssvacl  13641  lssvsubcl  13642  lssvscl  13651  lsslss  13657  lss1d  13659  lsspropdg  13707  opnssneib  14039  restbasg  14051  restopn2  14066  iscnp4  14101  cnss2  14110  cnconst2  14116  cnptopresti  14121  cnptoprest2  14123  neitx  14151  uptx  14157  txrest  14159  txdis1cn  14161  xmetres2  14262  xblss2ps  14287  blhalf  14291  blssps  14310  blss  14311  blssexps  14312  blssex  14313  blin2  14315  metequiv2  14379  bdmetval  14383  metcnp3  14394  metcnp  14395  metcn  14397  metcnpi  14398  metcnpi2  14399  txmetcnp  14401  txmetcn  14402  qtopbas  14405  tgqioo  14430  fsumcncntop  14439  elcncf2  14444  mulcncflem  14473  mulcncf  14474  suplociccreex  14485  limcdifap  14514  cnplimcim  14519  cnplimccntop  14522  limccnpcntop  14527  dvcj  14556  dveflem  14570  reeff1olem  14575  eflt  14579  sin0pilem1  14585  ptolemy  14628  coseq0q4123  14638  coseq0negpitopi  14640  cos02pilt1  14655  cos11  14657  ioocosf1o  14658  cxplt  14719  cxple  14720  cxplt3  14723  apcxp2  14741  rprelogbmul  14756  rprelogbdiv  14758  lgsval  14788  lgsfcl2  14790  lgscllem  14791  lgsval2lem  14794  lgsdir2lem4  14815  lgsdir2lem5  14816  lgsdir2  14817  lgsne0  14822  2sqlem6  14850  2sqlem10  14855  pwle2  15132  pwf1oexmid  15133  subctctexmid  15134  pw1nct  15136  peano4nninf  15139  nninfalllem1  15141  nninfall  15142  nninfsellemeq  15147  nninfsellemqall  15148  sbthom  15158  refeq  15160  isomninnlem  15162  trilpolemeq1  15172  trilpolemlt1  15173  trirec0  15176  apdiff  15180  iswomninnlem  15181  ismkvnnlem  15184  redcwlpolemeq1  15186  ltlenmkv  15202