Theorem simpllr 536

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

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

Proof of Theorem simpllr

Step	Hyp	Ref	Expression
1		simpr 110	. 2 |- ( ( ph /\ ps ) -> ps )
2	1	ad2antrr 488	1 |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> 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:  simp-4r  544  f1o2ndf1  6392  tfrlem1  6473  tfr1onlemaccex  6513  tfrcllemaccex  6526  frecabcl  6564  fopwdom  7021  phplem4dom  7047  phpm  7051  phplem4on  7053  fidifsnen  7056  diffisn  7081  diffifi  7082  en2eqpr  7098  fisseneq  7126  suplub2ti  7199  difinfsn  7298  ctmlemr  7306  ctm  7307  ctssdclemn0  7308  ctssdc  7311  nninfninc  7321  nninfisol  7331  enomnilem  7336  enmkvlem  7359  enwomnilem  7367  nninfwlpoimlemginf  7374  exmidontriimlem4  7438  exmidontriim  7439  cc3  7486  addcmpblnq  7586  mulcmpblnq  7587  ordpipqqs  7593  ltexnqq  7627  enq0tr  7653  addcmpblnq0  7662  mulcmpblnq0  7663  nnnq0lem1  7665  prssnqu  7699  prarloclemup  7714  nqprl  7770  nqpru  7771  mullocpr  7790  cauappcvgprlemladdfu  7873  cauappcvgprlemladdrl  7876  caucvgprlemm  7887  caucvgprlemladdfu  7896  caucvgprlemladdrl  7897  caucvgprlemlim  7900  caucvgprprlemml  7913  caucvgprprlemloc  7922  caucvgprprlemlim  7930  suplocexprlemmu  7937  suplocexprlemru  7938  suplocexprlemdisj  7939  suplocexprlemloc  7940  addcmpblnr  7958  mulcmpblnrlemg  7959  mulcmpblnr  7960  ltsrprg  7966  srpospr  8002  caucvgsrlemoffres  8019  suplocsrlemb  8025  suplocsrlempr  8026  suplocsrlem  8027  axcaucvglemcau  8117  axsuploc  8251  cnegexlem3  8355  negeu  8369  add20  8653  rimul  8764  apreap  8766  cru  8781  apreim  8782  apsym  8785  apcotr  8786  apadd1  8787  apneg  8790  mulext1  8791  apti  8801  aptap  8829  mulap0  8833  prodgt0  9031  ltmul12a  9039  ledivdiv  9069  lediv12a  9073  supinfneg  9828  infsupneg  9829  qapne  9872  xaddf  10078  xaddval  10079  xleadd1a  10107  xleaddadd  10121  ixxss12  10140  ioodisj  10227  fznlem  10275  zsupcllemstep  10488  qtri3or  10499  exbtwnzlemstep  10506  rebtwn2zlemstep  10511  addmodlteq  10659  seqf1og  10782  mulexpzap  10840  leexp1a  10855  expnbnd  10924  apexp1  10979  faclbnd  11002  hashxp  11089  zfz1iso  11104  swrdswrdlem  11284  cjap  11466  caucvgre  11541  cvg1nlemres  11545  resqrexlemglsq  11582  resqrexlemga  11583  sqrtsq  11604  ltabs  11647  abs3lem  11671  cau3lem  11674  maxleim  11765  rexico  11781  minmax  11790  xrmaxleim  11804  xrmaxiflemcl  11805  xrmaxiflemlub  11808  xrmaxiflemval  11810  xrmaxltsup  11818  xrmaxadd  11821  xrminmax  11825  xrbdtri  11836  climcau  11907  climrecvg1n  11908  sumeq2  11919  summodclem2  11942  divcnv  12057  prodeq2  12117  fprodsplitdc  12156  fprodconst  12180  dvdsle  12404  bitsfzo  12515  dvdsbnd  12526  bezoutlemmain  12568  bezoutlemzz  12572  bezoutlembi  12575  dfgcd3  12580  dvdsmulgcd  12595  nnmindc  12604  lcmcllem  12638  lcmgcdlem  12648  ncoprmgcdne1b  12660  isprm5  12713  pw2dvdslemn  12736  oddpwdclemxy  12740  pythagtriplem2  12838  pythagtrip  12855  pceu  12867  pc2dvds  12902  pcz  12904  pcadd  12912  pcfac  12922  exmidunben  13046  ctiunctlemfo  13059  unct  13062  prdsval  13355  sgrppropd  13495  sgrpidmndm  13502  mndpropd  13522  mhmeql  13574  isgrpinv  13636  dfgrp3mlem  13680  mhmmnd  13702  conjnmzb  13866  ghmcmn  13913  gsumfzconst  13927  isrng  13946  issrg  13977  isring  14012  dvdsrmul1  14115  tgrest  14892  cnpnei  14942  cnss1  14949  cncnp  14953  ismet2  15077  metequiv2  15219  metcnp  15235  metcnp2  15236  metcnpi3  15240  fsumcncntop  15290  elcncf2  15297  cncfmet  15315  suplociccreex  15347  dedekindicclemicc  15355  ivthinclemlr  15360  ivthinclemur  15362  cnplimclemr  15392  limccnpcntop  15398  limccoap  15401  dvmptfsum  15448  elply2  15458  plyrecj  15486  mersenne  15720  lgsval2lem  15738  lgsquad3  15812  usgr1eop  16095  usgr1vr  16098  pw1ndom3  16589  nninfalllem1  16610  nnnninfex  16624  sbthom  16630  apdiff  16652