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  6393  tfrlem1  6474  tfr1onlemaccex  6514  tfrcllemaccex  6527  frecabcl  6565  fopwdom  7022  phplem4dom  7048  phpm  7052  phplem4on  7054  fidifsnen  7057  diffisn  7082  diffifi  7083  en2eqpr  7099  fisseneq  7127  suplub2ti  7200  difinfsn  7299  ctmlemr  7307  ctm  7308  ctssdclemn0  7309  ctssdc  7312  nninfninc  7322  nninfisol  7332  enomnilem  7337  enmkvlem  7360  enwomnilem  7368  nninfwlpoimlemginf  7375  exmidontriimlem4  7439  exmidontriim  7440  cc3  7487  addcmpblnq  7587  mulcmpblnq  7588  ordpipqqs  7594  ltexnqq  7628  enq0tr  7654  addcmpblnq0  7663  mulcmpblnq0  7664  nnnq0lem1  7666  prssnqu  7700  prarloclemup  7715  nqprl  7771  nqpru  7772  mullocpr  7791  cauappcvgprlemladdfu  7874  cauappcvgprlemladdrl  7877  caucvgprlemm  7888  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  caucvgprlemlim  7901  caucvgprprlemml  7914  caucvgprprlemloc  7923  caucvgprprlemlim  7931  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemloc  7941  addcmpblnr  7959  mulcmpblnrlemg  7960  mulcmpblnr  7961  ltsrprg  7967  srpospr  8003  caucvgsrlemoffres  8020  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  axcaucvglemcau  8118  axsuploc  8252  cnegexlem3  8356  negeu  8370  add20  8654  rimul  8765  apreap  8767  cru  8782  apreim  8783  apsym  8786  apcotr  8787  apadd1  8788  apneg  8791  mulext1  8792  apti  8802  aptap  8830  mulap0  8834  prodgt0  9032  ltmul12a  9040  ledivdiv  9070  lediv12a  9074  supinfneg  9829  infsupneg  9830  qapne  9873  xaddf  10079  xaddval  10080  xleadd1a  10108  xleaddadd  10122  ixxss12  10141  ioodisj  10228  fznlem  10276  zsupcllemstep  10490  qtri3or  10501  exbtwnzlemstep  10508  rebtwn2zlemstep  10513  addmodlteq  10661  seqf1og  10784  mulexpzap  10842  leexp1a  10857  expnbnd  10926  apexp1  10981  faclbnd  11004  hashxp  11091  zfz1iso  11106  swrdswrdlem  11289  cjap  11484  caucvgre  11559  cvg1nlemres  11563  resqrexlemglsq  11600  resqrexlemga  11601  sqrtsq  11622  ltabs  11665  abs3lem  11689  cau3lem  11692  maxleim  11783  rexico  11799  minmax  11808  xrmaxleim  11822  xrmaxiflemcl  11823  xrmaxiflemlub  11826  xrmaxiflemval  11828  xrmaxltsup  11836  xrmaxadd  11839  xrminmax  11843  xrbdtri  11854  climcau  11925  climrecvg1n  11926  sumeq2  11937  summodclem2  11961  divcnv  12076  prodeq2  12136  fprodsplitdc  12175  fprodconst  12199  dvdsle  12423  bitsfzo  12534  dvdsbnd  12545  bezoutlemmain  12587  bezoutlemzz  12591  bezoutlembi  12594  dfgcd3  12599  dvdsmulgcd  12614  nnmindc  12623  lcmcllem  12657  lcmgcdlem  12667  ncoprmgcdne1b  12679  isprm5  12732  pw2dvdslemn  12755  oddpwdclemxy  12759  pythagtriplem2  12857  pythagtrip  12874  pceu  12886  pc2dvds  12921  pcz  12923  pcadd  12931  pcfac  12941  exmidunben  13065  ctiunctlemfo  13078  unct  13081  prdsval  13374  sgrppropd  13514  sgrpidmndm  13521  mndpropd  13541  mhmeql  13593  isgrpinv  13655  dfgrp3mlem  13699  mhmmnd  13721  conjnmzb  13885  ghmcmn  13932  gsumfzconst  13946  isrng  13966  issrg  13997  isring  14032  dvdsrmul1  14135  tgrest  14912  cnpnei  14962  cnss1  14969  cncnp  14973  ismet2  15097  metequiv2  15239  metcnp  15255  metcnp2  15256  metcnpi3  15260  fsumcncntop  15310  elcncf2  15317  cncfmet  15335  suplociccreex  15367  dedekindicclemicc  15375  ivthinclemlr  15380  ivthinclemur  15382  cnplimclemr  15412  limccnpcntop  15418  limccoap  15421  dvmptfsum  15468  elply2  15478  plyrecj  15506  mersenne  15740  lgsval2lem  15758  lgsquad3  15832  usgr1eop  16115  usgr1vr  16118  pw1ndom3  16640  nninfalllem1  16661  nnnninfex  16675  sbthom  16681  apdiff  16703