Theorem simpllr 523

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 479	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  531  f1o2ndf1  6125  tfrlem1  6205  tfr1onlemaccex  6245  tfrcllemaccex  6258  frecabcl  6296  fopwdom  6730  phplem4dom  6756  phpm  6759  phplem4on  6761  fidifsnen  6764  diffisn  6787  diffifi  6788  en2eqpr  6801  fisseneq  6820  suplub2ti  6888  difinfsn  6985  ctmlemr  6993  ctm  6994  ctssdclemn0  6995  ctssdc  6998  enomnilem  7010  addcmpblnq  7175  mulcmpblnq  7176  ordpipqqs  7182  ltexnqq  7216  enq0tr  7242  addcmpblnq0  7251  mulcmpblnq0  7252  nnnq0lem1  7254  prssnqu  7288  prarloclemup  7303  nqprl  7359  nqpru  7360  mullocpr  7379  cauappcvgprlemladdfu  7462  cauappcvgprlemladdrl  7465  caucvgprlemm  7476  caucvgprlemladdfu  7485  caucvgprlemladdrl  7486  caucvgprlemlim  7489  caucvgprprlemml  7502  caucvgprprlemloc  7511  caucvgprprlemlim  7519  suplocexprlemmu  7526  suplocexprlemru  7527  suplocexprlemdisj  7528  suplocexprlemloc  7529  addcmpblnr  7547  mulcmpblnrlemg  7548  mulcmpblnr  7549  ltsrprg  7555  srpospr  7591  caucvgsrlemoffres  7608  suplocsrlemb  7614  suplocsrlempr  7615  suplocsrlem  7616  axcaucvglemcau  7706  axsuploc  7837  cnegexlem3  7939  negeu  7953  add20  8236  rimul  8347  apreap  8349  cru  8364  apreim  8365  apsym  8368  apcotr  8369  apadd1  8370  apneg  8373  mulext1  8374  apti  8384  mulap0  8415  prodgt0  8610  ltmul12a  8618  ledivdiv  8648  lediv12a  8652  supinfneg  9390  infsupneg  9391  qapne  9431  xaddf  9627  xaddval  9628  xleadd1a  9656  xleaddadd  9670  ixxss12  9689  ioodisj  9776  fznlem  9821  qtri3or  10020  exbtwnzlemstep  10025  rebtwn2zlemstep  10030  addmodlteq  10171  mulexpzap  10333  leexp1a  10348  expnbnd  10415  faclbnd  10487  hashxp  10572  zfz1iso  10584  cjap  10678  caucvgre  10753  cvg1nlemres  10757  resqrexlemglsq  10794  resqrexlemga  10795  sqrtsq  10816  ltabs  10859  abs3lem  10883  cau3lem  10886  maxleim  10977  rexico  10993  minmax  11001  xrmaxleim  11013  xrmaxiflemcl  11014  xrmaxiflemlub  11017  xrmaxiflemval  11019  xrmaxltsup  11027  xrmaxadd  11030  xrminmax  11034  xrbdtri  11045  climcau  11116  climrecvg1n  11117  sumeq2  11128  summodclem2  11151  divcnv  11266  prodeq2  11326  dvdsle  11542  zsupcllemstep  11638  dvdsbnd  11645  gcdsupex  11646  gcdsupcl  11647  bezoutlemmain  11686  bezoutlemzz  11690  bezoutlembi  11693  dfgcd3  11698  dvdsmulgcd  11713  lcmcllem  11748  lcmgcdlem  11758  ncoprmgcdne1b  11770  pw2dvdslemn  11843  oddpwdclemxy  11847  exmidunben  11939  ctiunctlemfo  11952  unct  11954  tgrest  12338  cnpnei  12388  cnss1  12395  cncnp  12399  ismet2  12523  metequiv2  12665  metcnp  12681  metcnp2  12682  metcnpi3  12686  fsumcncntop  12725  elcncf2  12730  cncfmet  12748  suplociccreex  12771  dedekindicclemicc  12779  ivthinclemlr  12784  ivthinclemur  12786  cnplimclemr  12807  limccnpcntop  12813  limccoap  12816  nninfalllem1  13203  sbthom  13221