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  3524  intab  3858  exmid01  4182  exmidundif  4190  exmidundifim  4191  frirrg  4333  reg2exmidlema  4516  imadiflem  5275  fvco4  5566  fvmptt  5585  fcoconst  5664  f1imass  5750  fcof1  5759  fliftfun  5772  riotass2  5832  ovmpodxf  5975  dftpos4  6239  tfrlem1  6284  tfrlem3ag  6285  tfrlemibacc  6302  tfrlemibfn  6304  tfrlemi1  6308  tfrlemi14d  6309  tfr1onlem3ag  6313  tfr1onlembacc  6318  tfr1onlembfn  6320  tfr1onlemaccex  6324  tfrcllembacc  6331  tfrcllembfn  6333  tfrcllemaccex  6337  frecabcl  6375  nntr2  6479  dcdifsnid  6480  nnm00  6505  ecopovsymg  6608  ecopoverg  6610  th3qlem1  6611  mapss  6665  f1imaen2g  6767  xpen  6819  xpmapenlem  6823  phpm  6839  fidifsnen  6844  dif1enen  6854  fiunsnnn  6855  fin0  6859  fin0or  6860  findcard2d  6865  findcard2sd  6866  diffifi  6868  isinfinf  6871  tridc  6873  fimax2gtrilemstep  6874  fimax2gtri  6875  en2eqpr  6881  onunsnss  6890  unsnfidcex  6893  unsnfidcel  6894  undifdcss  6896  unfiin  6899  fisseneq  6905  ssfirab  6907  f1finf1o  6920  fidcenumlemrks  6926  fidcenumlemrk  6927  fidcenumlemr  6928  fidcenum  6929  suplub2ti  6974  supisolem  6981  ordiso2  7008  djudom  7066  omp1eomlem  7067  difinfsnlem  7072  difinfinf  7074  ctm  7082  ctssdclemn0  7083  enumct  7088  nnnninfeq  7100  nnnninfeq2  7101  nninfisol  7105  enomnilem  7110  finomni  7112  exmidomni  7114  fodju0  7119  ismkvnex  7127  enmkvlem  7133  enwomnilem  7141  exmidfodomrlemr  7166  exmidfodomrlemrALT  7167  exmidaclem  7172  exmidontriimlem1  7185  exmidontriimlem2  7186  exmidontriimlem3  7187  exmidontriimlem4  7188  exmidontriim  7189  dfplpq2  7303  dfmpq2  7304  mulpipqqs  7322  nqpi  7327  distrnqg  7336  prarloclemarch  7367  enq0tr  7383  nqnq0pi  7387  nq0nn  7391  nnnq0lem1  7395  prarloclemup  7444  prarloclem3  7446  prarloclemcalc  7451  genplt2i  7459  addnqprllem  7476  addnqprulem  7477  appdivnq  7512  distrlem1prl  7531  distrlem1pru  7532  ltaddpr  7546  ltexprlemlol  7551  ltexprlemupu  7553  ltexprlemdisj  7555  addcanprleml  7563  ltaprlem  7567  addextpr  7570  recexprlemopu  7576  recexprlemdisj  7579  recexprlem1ssl  7582  aptiprleml  7588  cauappcvgprlemm  7594  cauappcvgprlemopl  7595  cauappcvgprlemlol  7596  cauappcvgprlemopu  7597  cauappcvgprlemdisj  7600  cauappcvgprlemladdfu  7603  cauappcvgprlemladdfl  7604  cauappcvgprlemladdru  7605  cauappcvgprlemladdrl  7606  caucvgprlemm  7617  caucvgprlemopl  7618  caucvgprlemlol  7619  caucvgprlemopu  7620  caucvgprlemladdfu  7626  caucvgprprlemml  7643  caucvgprprlemopl  7646  caucvgprprlemlol  7647  caucvgprprlemopu  7648  caucvgprprlemexbt  7655  suplocexprlemru  7668  suplocexprlemloc  7670  suplocexprlemub  7672  suplocexprlemlub  7673  prsrlem1  7691  recexgt0sr  7722  mulgt0sr  7727  archsr  7731  caucvgsrlemcau  7742  caucvgsrlemoffcau  7747  caucvgsrlemoffres  7749  suplocsrlemb  7755  suplocsrlempr  7756  suplocsrlem  7757  addcnsr  7783  mulcnsr  7784  mulcnsrec  7792  axmulcom  7820  nntopi  7843  axcaucvglemcau  7847  axcaucvglemres  7848  axpre-suploclemres  7850  axpre-suploc  7851  axsuploc  7979  ltntri  8034  cnegexlem2  8082  cnegexlem3  8083  addsub4  8149  le2add  8350  lt2add  8351  lt2sub  8366  le2sub  8367  rereim  8492  apreim  8509  mulreim  8510  apcotr  8513  apadd1  8514  addext  8516  mulext1  8518  mulext  8520  apti  8528  receuap  8574  rec11rap  8615  divdivdivap  8617  divadddivap  8631  divsubdivap  8632  rerecclap  8634  recgt0  8753  prodgt0gt0  8754  prodgt0  8755  prodge0  8757  lemulge11  8769  lt2mul2div  8782  ltrec  8786  lerec  8787  ltrec1  8791  lediv2a  8798  mulle0r  8847  sup3exmid  8860  zdiv  9287  eluzuzle  9482  supinfneg  9541  infsupneg  9542  infregelbex  9544  xrltso  9740  xnn0dcle  9746  xnn0letri  9747  npnflt  9759  nmnfgt  9762  z2ge  9770  xaddf  9788  xaddval  9789  xpncan  9815  xleadd1a  9817  xltadd1  9820  xaddge0  9822  xle2add  9823  xleaddadd  9831  ixxss1  9848  ixxss2  9849  elico2  9881  iccsupr  9910  fzass4  10005  fzrev  10027  fz0fzelfz0  10070  fzocatel  10142  elfzomelpfzo  10174  exbtwnzlemstep  10191  rebtwn2zlemstep  10196  qbtwnxr  10201  apbtwnz  10217  btwnzge0  10243  modqid  10292  modqcyc  10302  modqcyc2  10303  modqaddabs  10305  modqaddmod  10306  mulqaddmodid  10307  modqmuladd  10309  modqltm1p1mod  10319  modqsubmod  10325  modqsubmodmod  10326  modaddmodlo  10331  modqmulmod  10332  modqmulmodr  10333  modqsubdir  10336  addmodlteq  10341  iseqf1olemab  10432  iseqf1olemmo  10435  iseqf1olemjpcl  10438  iseqf1olemqpcl  10439  exp3val  10465  expcl2lemap  10475  expap0  10493  expnegzap  10497  expmul  10508  leexp1a  10518  qsqeqor  10573  expnbnd  10586  nn0ltexp2  10631  nn0opth2  10645  facndiv  10660  faclbnd  10662  bcval5  10684  bcpasc  10687  hashennnuni  10700  hashunlem  10726  hashunsng  10729  hashprg  10730  fiprsshashgt1  10739  hashxp  10748  fimaxq  10749  zfz1isolemiso  10761  zfz1isolem1  10762  seq3coll  10764  shftlem  10767  shftfvalg  10769  shftfval  10772  2shfti  10782  caucvgrelemrec  10930  caucvgrelemcau  10931  caucvgre  10932  cvg1nlemcau  10935  cvg1nlemres  10936  resqrexlemcalc3  10967  resqrexlemcvg  10970  resqrexlemglsq  10973  resqrexlemga  10974  sqrtsq  10995  leabs  11025  absexpzap  11031  abslt  11039  absle  11040  abssubap0  11041  caubnd2  11068  icodiamlt  11131  maxleim  11156  maxabslemval  11159  maxleastlt  11166  rexico  11172  zmaxcl  11175  fimaxre2  11177  minmax  11180  xrmaxleim  11194  xrmaxiflemcl  11195  xrmaxifle  11196  xrmaxiflemlub  11198  xrmaxiflemval  11200  xrmaxleastlt  11206  xrmaxltsup  11208  xrmaxadd  11211  xrminmax  11215  xrbdtri  11226  climuni  11243  climshftlemg  11252  iserex  11289  climcau  11297  climrecvg1n  11298  climcvg1nlem  11299  sumeq2  11309  summodclem3  11330  zsumdc  11334  isumss  11341  fisumss  11342  sumsnf  11359  fsumconst  11404  modfsummod  11408  fsum00  11412  fsumabs  11415  fsumrelem  11421  fsumiun  11427  isumsplit  11441  divcnv  11447  geo2sum  11464  geoisumr  11468  cvgratz  11482  ntrivcvgap  11498  prodeq2  11507  prodmodclem2  11527  prodmodc  11528  zproddc  11529  fprodmul  11541  prodsnf  11542  fprodcl2lem  11555  fprodconst  11570  fprodap0  11571  fprodrec  11579  fprodap0f  11586  fprodle  11590  fprodmodd  11591  tanaddap  11689  zdvdsdc  11761  dvds2ln  11773  dvdsle  11791  dvdsext  11802  divalglemeunn  11867  divalglemex  11868  divalglemeuneg  11869  zsupcllemstep  11887  dvdsbnd  11898  gcdsupex  11899  gcdsupcl  11900  dvdslegcd  11906  bezoutlemnewy  11938  bezoutlemstep  11939  bezoutlemmain  11940  bezoutlemzz  11944  bezoutlembz  11946  bezoutlembi  11947  bezoutlemle  11950  dfgcd3  11952  bezout  11953  dfgcd2  11956  dvdsmulgcd  11967  bezoutr  11974  uzwodc  11979  lcmval  12004  lcmcllem  12008  lcmneg  12015  ncoprmgcdne1b  12030  isprm2lem  12057  prmind2  12061  dvdsnprmd  12066  isprm5  12083  prmdvdsexp  12089  sqrt2irr  12103  oddpwdclemxy  12110  oddpwdclemdc  12114  nonsq  12148  pceu  12236  pcmul  12242  pc2dvds  12270  pcz  12272  pcprmpw2  12273  dvdsprmpweqle  12277  pcfac  12289  qexpz  12291  prmpwdvds  12294  1arith  12306  mul4sq  12333  ennnfonelemkh  12354  ennnfonelemhf1o  12355  ennnfonelemhom  12357  ennnfonelemfun  12359  ennnfonelemf1  12360  ennnfonelemim  12366  exmidunben  12368  ctiunctlemfo  12381  omiunct  12386  ssnnctlemct  12388  isstruct2r  12414  ismgm  12598  issgrp  12631  sgrpidmndm  12643  mndpropd  12663  opnssneib  12909  restbasg  12921  restopn2  12936  iscnp4  12971  cnss2  12980  cnconst2  12986  cnptopresti  12991  cnptoprest2  12993  neitx  13021  uptx  13027  txrest  13029  txdis1cn  13031  xmetres2  13132  xblss2ps  13157  blhalf  13161  blssps  13180  blss  13181  blssexps  13182  blssex  13183  blin2  13185  metequiv2  13249  bdmetval  13253  metcnp3  13264  metcnp  13265  metcn  13267  metcnpi  13268  metcnpi2  13269  txmetcnp  13271  txmetcn  13272  qtopbas  13275  tgqioo  13300  fsumcncntop  13309  elcncf2  13314  mulcncflem  13343  mulcncf  13344  suplociccreex  13355  limcdifap  13384  cnplimcim  13389  cnplimccntop  13392  limccnpcntop  13397  dvcj  13426  dveflem  13440  reeff1olem  13445  eflt  13449  sin0pilem1  13455  ptolemy  13498  coseq0q4123  13508  coseq0negpitopi  13510  cos02pilt1  13525  cos11  13527  ioocosf1o  13528  cxplt  13589  cxple  13590  cxplt3  13593  apcxp2  13611  rprelogbmul  13626  rprelogbdiv  13628  lgsval  13658  lgsfcl2  13660  lgscllem  13661  lgsval2lem  13664  lgsdir2lem4  13685  lgsdir2lem5  13686  lgsdir2  13687  lgsne0  13692  2sqlem6  13709  2sqlem10  13714  pwle2  13991  pwf1oexmid  13992  subctctexmid  13994  pw1nct  13996  peano4nninf  13999  nninfalllem1  14001  nninfall  14002  nninfsellemeq  14007  nninfsellemqall  14008  sbthom  14018  refeq  14020  isomninnlem  14022  trilpolemeq1  14032  trilpolemlt1  14033  trirec0  14036  apdiff  14040  iswomninnlem  14041  ismkvnnlem  14044  redcwlpolemeq1  14046