Theorem simplr 525

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 486	1 |- ( ( ( ph /\ ps ) /\ ch ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  simp1lr  1056  simp2lr  1060  simp3lr  1064  bilukdc  1391  dcun  3525  intab  3860  exmid01  4184  exmidundif  4192  exmidundifim  4193  frirrg  4335  reg2exmidlema  4518  imadiflem  5277  fvco4  5568  fvmptt  5587  fcoconst  5667  f1imass  5753  fcof1  5762  fliftfun  5775  riotass2  5835  ovmpodxf  5978  dftpos4  6242  tfrlem1  6287  tfrlem3ag  6288  tfrlemibacc  6305  tfrlemibfn  6307  tfrlemi1  6311  tfrlemi14d  6312  tfr1onlem3ag  6316  tfr1onlembacc  6321  tfr1onlembfn  6323  tfr1onlemaccex  6327  tfrcllembacc  6334  tfrcllembfn  6336  tfrcllemaccex  6340  frecabcl  6378  nntr2  6482  dcdifsnid  6483  nnm00  6509  ecopovsymg  6612  ecopoverg  6614  th3qlem1  6615  mapss  6669  f1imaen2g  6771  xpen  6823  xpmapenlem  6827  phpm  6843  fidifsnen  6848  dif1enen  6858  fiunsnnn  6859  fin0  6863  fin0or  6864  findcard2d  6869  findcard2sd  6870  diffifi  6872  isinfinf  6875  tridc  6877  fimax2gtrilemstep  6878  fimax2gtri  6879  en2eqpr  6885  onunsnss  6894  unsnfidcex  6897  unsnfidcel  6898  undifdcss  6900  unfiin  6903  fisseneq  6909  ssfirab  6911  f1finf1o  6924  fidcenumlemrks  6930  fidcenumlemrk  6931  fidcenumlemr  6932  fidcenum  6933  suplub2ti  6978  supisolem  6985  ordiso2  7012  djudom  7070  omp1eomlem  7071  difinfsnlem  7076  difinfinf  7078  ctm  7086  ctssdclemn0  7087  enumct  7092  nnnninfeq  7104  nnnninfeq2  7105  nninfisol  7109  enomnilem  7114  finomni  7116  exmidomni  7118  fodju0  7123  ismkvnex  7131  enmkvlem  7137  enwomnilem  7145  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  exmidaclem  7185  exmidontriimlem1  7198  exmidontriimlem2  7199  exmidontriimlem3  7200  exmidontriimlem4  7201  exmidontriim  7202  dfplpq2  7316  dfmpq2  7317  mulpipqqs  7335  nqpi  7340  distrnqg  7349  prarloclemarch  7380  enq0tr  7396  nqnq0pi  7400  nq0nn  7404  nnnq0lem1  7408  prarloclemup  7457  prarloclem3  7459  prarloclemcalc  7464  genplt2i  7472  addnqprllem  7489  addnqprulem  7490  appdivnq  7525  distrlem1prl  7544  distrlem1pru  7545  ltaddpr  7559  ltexprlemlol  7564  ltexprlemupu  7566  ltexprlemdisj  7568  addcanprleml  7576  ltaprlem  7580  addextpr  7583  recexprlemopu  7589  recexprlemdisj  7592  recexprlem1ssl  7595  aptiprleml  7601  cauappcvgprlemm  7607  cauappcvgprlemopl  7608  cauappcvgprlemlol  7609  cauappcvgprlemopu  7610  cauappcvgprlemdisj  7613  cauappcvgprlemladdfu  7616  cauappcvgprlemladdfl  7617  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  caucvgprlemm  7630  caucvgprlemopl  7631  caucvgprlemlol  7632  caucvgprlemopu  7633  caucvgprlemladdfu  7639  caucvgprprlemml  7656  caucvgprprlemopl  7659  caucvgprprlemlol  7660  caucvgprprlemopu  7661  caucvgprprlemexbt  7668  suplocexprlemru  7681  suplocexprlemloc  7683  suplocexprlemub  7685  suplocexprlemlub  7686  prsrlem1  7704  recexgt0sr  7735  mulgt0sr  7740  archsr  7744  caucvgsrlemcau  7755  caucvgsrlemoffcau  7760  caucvgsrlemoffres  7762  suplocsrlemb  7768  suplocsrlempr  7769  suplocsrlem  7770  addcnsr  7796  mulcnsr  7797  mulcnsrec  7805  axmulcom  7833  nntopi  7856  axcaucvglemcau  7860  axcaucvglemres  7861  axpre-suploclemres  7863  axpre-suploc  7864  axsuploc  7992  ltntri  8047  cnegexlem2  8095  cnegexlem3  8096  addsub4  8162  le2add  8363  lt2add  8364  lt2sub  8379  le2sub  8380  rereim  8505  apreim  8522  mulreim  8523  apcotr  8526  apadd1  8527  addext  8529  mulext1  8531  mulext  8533  apti  8541  receuap  8587  rec11rap  8628  divdivdivap  8630  divadddivap  8644  divsubdivap  8645  rerecclap  8647  recgt0  8766  prodgt0gt0  8767  prodgt0  8768  prodge0  8770  lemulge11  8782  lt2mul2div  8795  ltrec  8799  lerec  8800  ltrec1  8804  lediv2a  8811  mulle0r  8860  sup3exmid  8873  zdiv  9300  eluzuzle  9495  supinfneg  9554  infsupneg  9555  infregelbex  9557  xrltso  9753  xnn0dcle  9759  xnn0letri  9760  npnflt  9772  nmnfgt  9775  z2ge  9783  xaddf  9801  xaddval  9802  xpncan  9828  xleadd1a  9830  xltadd1  9833  xaddge0  9835  xle2add  9836  xleaddadd  9844  ixxss1  9861  ixxss2  9862  elico2  9894  iccsupr  9923  fzass4  10018  fzrev  10040  fz0fzelfz0  10083  fzocatel  10155  elfzomelpfzo  10187  exbtwnzlemstep  10204  rebtwn2zlemstep  10209  qbtwnxr  10214  apbtwnz  10230  btwnzge0  10256  modqid  10305  modqcyc  10315  modqcyc2  10316  modqaddabs  10318  modqaddmod  10319  mulqaddmodid  10320  modqmuladd  10322  modqltm1p1mod  10332  modqsubmod  10338  modqsubmodmod  10339  modaddmodlo  10344  modqmulmod  10345  modqmulmodr  10346  modqsubdir  10349  addmodlteq  10354  iseqf1olemab  10445  iseqf1olemmo  10448  iseqf1olemjpcl  10451  iseqf1olemqpcl  10452  exp3val  10478  expcl2lemap  10488  expap0  10506  expnegzap  10510  expmul  10521  leexp1a  10531  qsqeqor  10586  expnbnd  10599  nn0ltexp2  10644  nn0opth2  10658  facndiv  10673  faclbnd  10675  bcval5  10697  bcpasc  10700  hashennnuni  10713  hashunlem  10739  hashunsng  10742  hashprg  10743  fiprsshashgt1  10752  hashxp  10761  fimaxq  10762  zfz1isolemiso  10774  zfz1isolem1  10775  seq3coll  10777  shftlem  10780  shftfvalg  10782  shftfval  10785  2shfti  10795  caucvgrelemrec  10943  caucvgrelemcau  10944  caucvgre  10945  cvg1nlemcau  10948  cvg1nlemres  10949  resqrexlemcalc3  10980  resqrexlemcvg  10983  resqrexlemglsq  10986  resqrexlemga  10987  sqrtsq  11008  leabs  11038  absexpzap  11044  abslt  11052  absle  11053  abssubap0  11054  caubnd2  11081  icodiamlt  11144  maxleim  11169  maxabslemval  11172  maxleastlt  11179  rexico  11185  zmaxcl  11188  fimaxre2  11190  minmax  11193  xrmaxleim  11207  xrmaxiflemcl  11208  xrmaxifle  11209  xrmaxiflemlub  11211  xrmaxiflemval  11213  xrmaxleastlt  11219  xrmaxltsup  11221  xrmaxadd  11224  xrminmax  11228  xrbdtri  11239  climuni  11256  climshftlemg  11265  iserex  11302  climcau  11310  climrecvg1n  11311  climcvg1nlem  11312  sumeq2  11322  summodclem3  11343  zsumdc  11347  isumss  11354  fisumss  11355  sumsnf  11372  fsumconst  11417  modfsummod  11421  fsum00  11425  fsumabs  11428  fsumrelem  11434  fsumiun  11440  isumsplit  11454  divcnv  11460  geo2sum  11477  geoisumr  11481  cvgratz  11495  ntrivcvgap  11511  prodeq2  11520  prodmodclem2  11540  prodmodc  11541  zproddc  11542  fprodmul  11554  prodsnf  11555  fprodcl2lem  11568  fprodconst  11583  fprodap0  11584  fprodrec  11592  fprodap0f  11599  fprodle  11603  fprodmodd  11604  tanaddap  11702  zdvdsdc  11774  dvds2ln  11786  dvdsle  11804  dvdsext  11815  divalglemeunn  11880  divalglemex  11881  divalglemeuneg  11882  zsupcllemstep  11900  dvdsbnd  11911  gcdsupex  11912  gcdsupcl  11913  dvdslegcd  11919  bezoutlemnewy  11951  bezoutlemstep  11952  bezoutlemmain  11953  bezoutlemzz  11957  bezoutlembz  11959  bezoutlembi  11960  bezoutlemle  11963  dfgcd3  11965  bezout  11966  dfgcd2  11969  dvdsmulgcd  11980  bezoutr  11987  uzwodc  11992  lcmval  12017  lcmcllem  12021  lcmneg  12028  ncoprmgcdne1b  12043  isprm2lem  12070  prmind2  12074  dvdsnprmd  12079  isprm5  12096  prmdvdsexp  12102  sqrt2irr  12116  oddpwdclemxy  12123  oddpwdclemdc  12127  nonsq  12161  pceu  12249  pcmul  12255  pc2dvds  12283  pcz  12285  pcprmpw2  12286  dvdsprmpweqle  12290  pcfac  12302  qexpz  12304  prmpwdvds  12307  1arith  12319  mul4sq  12346  ennnfonelemkh  12367  ennnfonelemhf1o  12368  ennnfonelemhom  12370  ennnfonelemfun  12372  ennnfonelemf1  12373  ennnfonelemim  12379  exmidunben  12381  ctiunctlemfo  12394  omiunct  12399  ssnnctlemct  12401  isstruct2r  12427  ismgm  12611  issgrp  12644  sgrpidmndm  12656  mndpropd  12676  isgrpinv  12756  opnssneib  12950  restbasg  12962  restopn2  12977  iscnp4  13012  cnss2  13021  cnconst2  13027  cnptopresti  13032  cnptoprest2  13034  neitx  13062  uptx  13068  txrest  13070  txdis1cn  13072  xmetres2  13173  xblss2ps  13198  blhalf  13202  blssps  13221  blss  13222  blssexps  13223  blssex  13224  blin2  13226  metequiv2  13290  bdmetval  13294  metcnp3  13305  metcnp  13306  metcn  13308  metcnpi  13309  metcnpi2  13310  txmetcnp  13312  txmetcn  13313  qtopbas  13316  tgqioo  13341  fsumcncntop  13350  elcncf2  13355  mulcncflem  13384  mulcncf  13385  suplociccreex  13396  limcdifap  13425  cnplimcim  13430  cnplimccntop  13433  limccnpcntop  13438  dvcj  13467  dveflem  13481  reeff1olem  13486  eflt  13490  sin0pilem1  13496  ptolemy  13539  coseq0q4123  13549  coseq0negpitopi  13551  cos02pilt1  13566  cos11  13568  ioocosf1o  13569  cxplt  13630  cxple  13631  cxplt3  13634  apcxp2  13652  rprelogbmul  13667  rprelogbdiv  13669  lgsval  13699  lgsfcl2  13701  lgscllem  13702  lgsval2lem  13705  lgsdir2lem4  13726  lgsdir2lem5  13727  lgsdir2  13728  lgsne0  13733  2sqlem6  13750  2sqlem10  13755  pwle2  14031  pwf1oexmid  14032  subctctexmid  14034  pw1nct  14036  peano4nninf  14039  nninfalllem1  14041  nninfall  14042  nninfsellemeq  14047  nninfsellemqall  14048  sbthom  14058  refeq  14060  isomninnlem  14062  trilpolemeq1  14072  trilpolemlt1  14073  trirec0  14076  apdiff  14080  iswomninnlem  14081  ismkvnnlem  14084  redcwlpolemeq1  14086