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  11069  shftfvalg  11071  shftfval  11074  2shfti  11084  caucvgrelemrec  11232  caucvgrelemcau  11233  caucvgre  11234  cvg1nlemcau  11237  cvg1nlemres  11238  resqrexlemcalc3  11269  resqrexlemcvg  11272  resqrexlemglsq  11275  resqrexlemga  11276  sqrtsq  11297  leabs  11327  absexpzap  11333  abslt  11341  absle  11342  abssubap0  11343  caubnd2  11370  icodiamlt  11433  maxleim  11458  maxabslemval  11461  maxleastlt  11468  rexico  11474  zmaxcl  11477  fimaxre2  11480  minmax  11483  xrmaxleim  11497  xrmaxiflemcl  11498  xrmaxifle  11499  xrmaxiflemlub  11501  xrmaxiflemval  11503  xrmaxleastlt  11509  xrmaxltsup  11511  xrmaxadd  11514  xrminmax  11518  xrbdtri  11529  climuni  11546  climshftlemg  11555  iserex  11592  climcau  11600  climrecvg1n  11601  climcvg1nlem  11602  sumeq2  11612  summodclem3  11633  zsumdc  11637  isumss  11644  fisumss  11645  sumsnf  11662  fsumconst  11707  modfsummod  11711  fsum00  11715  fsumabs  11718  fsumrelem  11724  fsumiun  11730  isumsplit  11744  divcnv  11750  geo2sum  11767  geoisumr  11771  cvgratz  11785  ntrivcvgap  11801  prodeq2  11810  prodmodclem2  11830  prodmodc  11831  zproddc  11832  fprodmul  11844  prodsnf  11845  fprodcl2lem  11858  fprodconst  11873  fprodap0  11874  fprodrec  11882  fprodap0f  11889  fprodle  11893  fprodmodd  11894  tanaddap  11992  zdvdsdc  12065  dvds2ln  12077  fsumdvds  12095  dvdsle  12097  dvdsext  12108  divalglemeunn  12174  divalglemex  12175  divalglemeuneg  12176  bitsfzo  12208  bitsmod  12209  bitsinv1lem  12214  bitsinv1  12215  dvdsbnd  12219  gcdsupex  12220  gcdsupcl  12221  dvdslegcd  12227  bezoutlemnewy  12259  bezoutlemstep  12260  bezoutlemmain  12261  bezoutlemzz  12265  bezoutlembz  12267  bezoutlembi  12268  bezoutlemle  12271  dfgcd3  12273  bezout  12274  dfgcd2  12277  dvdsmulgcd  12288  bezoutr  12295  uzwodc  12300  nninfctlemfo  12303  lcmval  12327  lcmcllem  12331  lcmneg  12338  ncoprmgcdne1b  12353  isprm2lem  12380  prmind2  12384  dvdsnprmd  12389  isprm5  12406  prmdvdsexp  12412  sqrt2irr  12426  oddpwdclemxy  12433  oddpwdclemdc  12437  nonsq  12471  pceu  12560  pcmul  12566  pc2dvds  12595  pcz  12597  pcprmpw2  12598  dvdsprmpweqle  12602  pcfac  12615  qexpz  12617  prmpwdvds  12620  1arith  12632  mul4sq  12659  4sqexercise2  12664  4sqlemsdc  12665  ennnfonelemkh  12725  ennnfonelemhf1o  12726  ennnfonelemhom  12728  ennnfonelemfun  12730  ennnfonelemf1  12731  ennnfonelemim  12737  exmidunben  12739  ctiunctlemfo  12752  omiunct  12757  ssnnctlemct  12759  isstruct2r  12785  prdsval  13047  ismgm  13131  issgrp  13177  sgrppropd  13187  sgrpidmndm  13194  mndpropd  13214  issubmnd  13216  prdsidlem  13221  resmhm2b  13263  gsumwmhm  13272  isgrpinv  13328  grplmulf1o  13348  dfgrp3mlem  13372  grplactcnv  13376  pwssub  13387  mhmid  13393  mhmmnd  13394  ghmgrp  13396  mulgval  13400  mulgfng  13402  mulgnnp1  13408  mulgnn0dir  13430  mulgneg2  13434  mhmmulg  13441  grpissubg  13472  isnsg  13480  isnsg3  13485  nmzsubg  13488  ghmmhmb  13532  ghmpreima  13544  ghmnsgpreima  13547  ghmf1  13551  ghmf1o  13553  conjghm  13554  conjnmz  13557  conjnmzb  13558  ghmcmn  13605  gsumfzconst  13619  issrg  13669  srglmhm  13697  srgrmhm  13698  isring  13704  ringadd2  13731  ringlghm  13765  ringrghm  13766  oppr1g  13786  reldvdsrsrg  13796  dvdsrvald  13797  dvdsrd  13798  dvdsrex  13802  dvdsrmul1  13806  unitgrp  13820  rhmopp  13880  subrgintm  13947  subrgpropd  13957  isdomn  13973  lmodprop2d  14052  lssvacl  14069  lssvsubcl  14070  lssvscl  14079  lsslss  14085  lss1d  14087  lsspropdg  14135  expghmap  14311  mulgghm2  14312  znunit  14363  znrrg  14364  mplvalcoe  14394  mplsubgfilemcl  14403  mplsubgfileminv  14404  mplsubgfi  14405  opnssneib  14570  restbasg  14582  restopn2  14597  iscnp4  14632  cnss2  14641  cnconst2  14647  cnptopresti  14652  cnptoprest2  14654  neitx  14682  uptx  14688  txrest  14690  txdis1cn  14692  xmetres2  14793  xblss2ps  14818  blhalf  14822  blssps  14841  blss  14842  blssexps  14843  blssex  14844  blin2  14846  metequiv2  14910  bdmetval  14914  metcnp3  14925  metcnp  14926  metcn  14928  metcnpi  14929  metcnpi2  14930  txmetcnp  14932  txmetcn  14933  qtopbas  14936  tgqioo  14969  mpomulcn  14980  fsumcncntop  14981  elcncf2  14988  mulcncflem  15021  mulcncf  15022  suplociccreex  15038  limcdifap  15076  cnplimcim  15081  cnplimccntop  15084  limccnpcntop  15089  dvcj  15123  dvmptfsum  15139  dveflem  15140  ply1termlem  15156  plyaddlem1  15161  plymullem1  15162  plycolemc  15172  plycjlemc  15174  plyrecj  15177  dvply1  15179  reeff1olem  15185  eflt  15189  sin0pilem1  15195  ptolemy  15238  coseq0q4123  15248  coseq0negpitopi  15250  cos02pilt1  15265  cos11  15267  ioocosf1o  15268  rpcxpmul2  15327  cxplt  15330  cxple  15331  cxplt3  15334  apcxp2  15353  rprelogbmul  15369  rprelogbdiv  15371  dvdsppwf1o  15403  perfect  15415  lgsval  15423  lgsfcl2  15425  lgscllem  15426  lgsval2lem  15429  lgsdir2lem4  15450  lgsdir2lem5  15451  lgsdir2  15452  lgsne0  15457  gausslemma2dlem1a  15477  gausslemma2dlem1f1o  15479  2sqlem6  15539  2sqlem10  15544  2omap  15865  pwle2  15868  pwf1oexmid  15869  subctctexmid  15870  pw1nct  15873  peano4nninf  15876  nninfalllem1  15878  nninfall  15879  nninfsellemeq  15884  nninfsellemqall  15885  nnnninfex  15892  nninfnfiinf  15893  sbthom  15898  refeq  15900  isomninnlem  15902  trilpolemeq1  15912  trilpolemlt1  15913  trirec0  15916  apdiff  15920  iswomninnlem  15921  ismkvnnlem  15924  redcwlpolemeq1  15926  ltlenmkv  15942