Theorem simpllr 524

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 109	. 2 |- ( ( ph /\ ps ) -> ps )
2	1	ad2antrr 480	1 |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> 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:  simp-4r  532  f1o2ndf1  6133  tfrlem1  6213  tfr1onlemaccex  6253  tfrcllemaccex  6266  frecabcl  6304  fopwdom  6738  phplem4dom  6764  phpm  6767  phplem4on  6769  fidifsnen  6772  diffisn  6795  diffifi  6796  en2eqpr  6809  fisseneq  6828  suplub2ti  6896  difinfsn  6993  ctmlemr  7001  ctm  7002  ctssdclemn0  7003  ctssdc  7006  enomnilem  7018  enmkvlem  7043  enwomnilem  7050  cc3  7100  addcmpblnq  7199  mulcmpblnq  7200  ordpipqqs  7206  ltexnqq  7240  enq0tr  7266  addcmpblnq0  7275  mulcmpblnq0  7276  nnnq0lem1  7278  prssnqu  7312  prarloclemup  7327  nqprl  7383  nqpru  7384  mullocpr  7403  cauappcvgprlemladdfu  7486  cauappcvgprlemladdrl  7489  caucvgprlemm  7500  caucvgprlemladdfu  7509  caucvgprlemladdrl  7510  caucvgprlemlim  7513  caucvgprprlemml  7526  caucvgprprlemloc  7535  caucvgprprlemlim  7543  suplocexprlemmu  7550  suplocexprlemru  7551  suplocexprlemdisj  7552  suplocexprlemloc  7553  addcmpblnr  7571  mulcmpblnrlemg  7572  mulcmpblnr  7573  ltsrprg  7579  srpospr  7615  caucvgsrlemoffres  7632  suplocsrlemb  7638  suplocsrlempr  7639  suplocsrlem  7640  axcaucvglemcau  7730  axsuploc  7861  cnegexlem3  7963  negeu  7977  add20  8260  rimul  8371  apreap  8373  cru  8388  apreim  8389  apsym  8392  apcotr  8393  apadd1  8394  apneg  8397  mulext1  8398  apti  8408  mulap0  8439  prodgt0  8634  ltmul12a  8642  ledivdiv  8672  lediv12a  8676  supinfneg  9417  infsupneg  9418  qapne  9458  xaddf  9657  xaddval  9658  xleadd1a  9686  xleaddadd  9700  ixxss12  9719  ioodisj  9806  fznlem  9852  qtri3or  10051  exbtwnzlemstep  10056  rebtwn2zlemstep  10061  addmodlteq  10202  mulexpzap  10364  leexp1a  10379  expnbnd  10446  apexp1  10496  faclbnd  10519  hashxp  10604  zfz1iso  10616  cjap  10710  caucvgre  10785  cvg1nlemres  10789  resqrexlemglsq  10826  resqrexlemga  10827  sqrtsq  10848  ltabs  10891  abs3lem  10915  cau3lem  10918  maxleim  11009  rexico  11025  minmax  11033  xrmaxleim  11045  xrmaxiflemcl  11046  xrmaxiflemlub  11049  xrmaxiflemval  11051  xrmaxltsup  11059  xrmaxadd  11062  xrminmax  11066  xrbdtri  11077  climcau  11148  climrecvg1n  11149  sumeq2  11160  summodclem2  11183  divcnv  11298  prodeq2  11358  dvdsle  11578  zsupcllemstep  11674  dvdsbnd  11681  gcdsupex  11682  gcdsupcl  11683  bezoutlemmain  11722  bezoutlemzz  11726  bezoutlembi  11729  dfgcd3  11734  dvdsmulgcd  11749  lcmcllem  11784  lcmgcdlem  11794  ncoprmgcdne1b  11806  pw2dvdslemn  11879  oddpwdclemxy  11883  exmidunben  11975  ctiunctlemfo  11988  unct  11991  tgrest  12377  cnpnei  12427  cnss1  12434  cncnp  12438  ismet2  12562  metequiv2  12704  metcnp  12720  metcnp2  12721  metcnpi3  12725  fsumcncntop  12764  elcncf2  12769  cncfmet  12787  suplociccreex  12810  dedekindicclemicc  12818  ivthinclemlr  12823  ivthinclemur  12825  cnplimclemr  12846  limccnpcntop  12852  limccoap  12855  nninfalllem1  13378  sbthom  13396  apdiff  13416