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  6424  tfrlem1  6539  tfr1onlemaccex  6579  tfrcllemaccex  6592  frecabcl  6630  fopwdom  7089  phplem4dom  7116  phpm  7120  phplem4on  7122  fidifsnen  7125  diffisn  7150  diffifi  7151  en2eqpr  7167  fisseneq  7195  suplub2ti  7292  difinfsn  7391  ctmlemr  7399  ctm  7400  ctssdclemn0  7401  ctssdc  7404  nninfninc  7414  nninfisol  7424  enomnilem  7429  enmkvlem  7452  enwomnilem  7460  nninfwlpoimlemginf  7467  exmidontriimlem4  7531  exmidontriim  7532  cc3  7582  addcmpblnq  7682  mulcmpblnq  7683  ordpipqqs  7689  ltexnqq  7723  enq0tr  7749  addcmpblnq0  7758  mulcmpblnq0  7759  nnnq0lem1  7761  prssnqu  7795  prarloclemup  7810  nqprl  7866  nqpru  7867  mullocpr  7886  cauappcvgprlemladdfu  7969  cauappcvgprlemladdrl  7972  caucvgprlemm  7983  caucvgprlemladdfu  7992  caucvgprlemladdrl  7993  caucvgprlemlim  7996  caucvgprprlemml  8009  caucvgprprlemloc  8018  caucvgprprlemlim  8026  suplocexprlemmu  8033  suplocexprlemru  8034  suplocexprlemdisj  8035  suplocexprlemloc  8036  addcmpblnr  8054  mulcmpblnrlemg  8055  mulcmpblnr  8056  ltsrprg  8062  srpospr  8098  caucvgsrlemoffres  8115  suplocsrlemb  8121  suplocsrlempr  8122  suplocsrlem  8123  axcaucvglemcau  8213  axsuploc  8346  cnegexlem3  8450  negeu  8464  add20  8748  rimul  8859  apreap  8861  cru  8876  apreim  8877  apsym  8880  apcotr  8881  apadd1  8882  apneg  8885  mulext1  8886  apti  8896  aptap  8924  mulap0  8928  prodgt0  9126  ltmul12a  9134  ledivdiv  9164  lediv12a  9168  supinfneg  9927  infsupneg  9928  qapne  9971  xaddf  10177  xaddval  10178  xleadd1a  10206  xleaddadd  10220  ixxss12  10239  ioodisj  10326  fznlem  10375  zsupcllemstep  10589  qtri3or  10600  exbtwnzlemstep  10607  rebtwn2zlemstep  10612  addmodlteq  10760  seqf1og  10883  mulexpzap  10941  leexp1a  10956  expnbnd  11025  apexp1  11080  faclbnd  11103  hashxp  11191  sshashneg  11205  zfz1iso  11213  swrdswrdlem  11396  cjap  11591  caucvgre  11666  cvg1nlemres  11670  resqrexlemglsq  11707  resqrexlemga  11708  sqrtsq  11729  ltabs  11772  abs3lem  11796  cau3lem  11799  maxleim  11890  rexico  11906  minmax  11915  xrmaxleim  11929  xrmaxiflemcl  11930  xrmaxiflemlub  11933  xrmaxiflemval  11935  xrmaxltsup  11943  xrmaxadd  11946  xrminmax  11950  xrbdtri  11961  climcau  12032  climrecvg1n  12033  sumeq2  12044  summodclem2  12068  divcnv  12183  prodeq2  12243  fprodsplitdc  12282  fprodconst  12306  dvdsle  12530  bitsfzo  12641  dvdsbnd  12652  bezoutlemmain  12694  bezoutlemzz  12698  bezoutlembi  12701  dfgcd3  12706  dvdsmulgcd  12721  nnmindc  12730  lcmcllem  12764  lcmgcdlem  12774  ncoprmgcdne1b  12786  isprm5  12839  pw2dvdslemn  12862  oddpwdclemxy  12866  pythagtriplem2  12964  pythagtrip  12981  pceu  12993  pc2dvds  13028  pcz  13030  pcadd  13038  pcfac  13048  exmidunben  13177  ctiunctlemfo  13190  unct  13193  prdsval  13486  sgrppropd  13626  sgrpidmndm  13633  mndpropd  13653  mhmeql  13705  isgrpinv  13767  dfgrp3mlem  13811  mhmmnd  13833  conjnmzb  13997  ghmcmn  14044  gsumfzconst  14058  isrng  14078  issrg  14109  isring  14144  dvdsrmul1  14247  aprlring  14434  tgrest  15034  cnpnei  15084  cnss1  15091  cncnp  15095  ismet2  15219  metequiv2  15361  metcnp  15377  metcnp2  15378  metcnpi3  15382  fsumcncntop  15432  elcncf2  15439  cncfmet  15457  suplociccreex  15489  dedekindicclemicc  15497  ivthinclemlr  15502  ivthinclemur  15504  cnplimclemr  15534  limccnpcntop  15540  limccoap  15543  dvmptfsum  15590  elply2  15600  plyrecj  15628  mersenne  15865  lgsval2lem  15883  lgsquad3  15957  usgr1eop  16240  usgr1vr  16243  pw1ndom3  16764  nninfalllem1  16786  nnnninfex  16800  sbthom  16806  apdiff  16832  trimul0or  16845