Theorem simpllr 502

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 473	1 |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  simp-4r  510  f1o2ndf1  6009  tfrlem1  6089  tfr1onlemaccex  6129  tfrcllemaccex  6142  frecabcl  6180  fopwdom  6608  phplem4dom  6634  phpm  6637  phplem4on  6639  fidifsnen  6642  diffisn  6665  diffifi  6666  en2eqpr  6679  fisseneq  6698  suplub2ti  6752  ctmlemr  6846  ctm  6847  enomnilem  6857  addcmpblnq  6989  mulcmpblnq  6990  ordpipqqs  6996  ltexnqq  7030  enq0tr  7056  addcmpblnq0  7065  mulcmpblnq0  7066  nnnq0lem1  7068  prssnqu  7102  prarloclemup  7117  nqprl  7173  nqpru  7174  mullocpr  7193  cauappcvgprlemladdfu  7276  cauappcvgprlemladdrl  7279  caucvgprlemm  7290  caucvgprlemladdfu  7299  caucvgprlemladdrl  7300  caucvgprlemlim  7303  caucvgprprlemml  7316  caucvgprprlemloc  7325  caucvgprprlemlim  7333  addcmpblnr  7348  mulcmpblnrlemg  7349  mulcmpblnr  7350  ltsrprg  7356  srpospr  7391  caucvgsrlemoffres  7408  axcaucvglemcau  7496  cnegexlem3  7722  negeu  7736  add20  8015  rimul  8125  apreap  8127  cru  8142  apreim  8143  apsym  8146  apcotr  8147  apadd1  8148  apneg  8151  mulext1  8152  apti  8162  mulap0  8186  prodgt0  8376  ltmul12a  8384  ledivdiv  8414  lediv12a  8418  supinfneg  9146  infsupneg  9147  qapne  9187  ixxss12  9387  ioodisj  9473  fznlem  9518  qtri3or  9717  exbtwnzlemstep  9722  rebtwn2zlemstep  9727  addmodlteq  9868  mulexpzap  10058  leexp1a  10073  expnbnd  10140  faclbnd  10212  hashxp  10297  zfz1iso  10309  cjap  10403  caucvgre  10477  cvg1nlemres  10481  resqrexlemglsq  10518  resqrexlemga  10519  sqrtsq  10540  ltabs  10583  abs3lem  10607  cau3lem  10610  maxleim  10701  rexico  10717  minmax  10724  climcau  10799  climrecvg1n  10800  sumeq2  10811  isummolem2  10835  divcnv  10954  dvdsle  11186  zsupcllemstep  11282  dvdsbnd  11289  gcdsupex  11290  gcdsupcl  11291  bezoutlemmain  11328  bezoutlemzz  11332  bezoutlembi  11335  dfgcd3  11340  dvdsmulgcd  11355  lcmcllem  11390  lcmgcdlem  11400  ncoprmgcdne1b  11412  pw2dvdslemn  11484  oddpwdclemxy  11488  elcncf2  11934  nninfalllem1  12202