Theorem simpllr 500

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 108	. 2 |- ( ( ph /\ ps ) -> ps )
2	1	ad2antrr 471	1 |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  simp-4r  508  f1o2ndf1  5869  tfrlem1  5946  fopwdom  6333  phplem4dom  6348  phpm  6351  phplem4on  6353  fidifsnen  6355  diffisn  6377  diffifi  6378  en2eqpr  6380  suplub2ti  6414  addcmpblnq  6557  mulcmpblnq  6558  ordpipqqs  6564  ltexnqq  6598  enq0tr  6624  addcmpblnq0  6633  mulcmpblnq0  6634  nnnq0lem1  6636  prssnqu  6670  prarloclemup  6685  nqprl  6741  nqpru  6742  mullocpr  6761  cauappcvgprlemladdfu  6844  cauappcvgprlemladdrl  6847  caucvgprlemm  6858  caucvgprlemladdfu  6867  caucvgprlemladdrl  6868  caucvgprlemlim  6871  caucvgprprlemml  6884  caucvgprprlemloc  6893  caucvgprprlemlim  6901  addcmpblnr  6916  mulcmpblnrlemg  6917  mulcmpblnr  6918  ltsrprg  6924  srpospr  6959  caucvgsrlemoffres  6976  axcaucvglemcau  7064  cnegexlem3  7285  negeu  7299  add20  7578  rimul  7685  apreap  7687  cru  7702  apreim  7703  apsym  7706  apcotr  7707  apadd1  7708  apneg  7711  mulext1  7712  apti  7722  mulap0  7744  prodgt0  7930  ltmul12a  7938  ledivdiv  7968  lediv12a  7972  supinfneg  8683  infsupneg  8684  qapne  8724  ixxss12  8929  ioodisj  9015  fznlem  9060  qtri3or  9252  qbtwnzlemstep  9257  rebtwn2zlemstep  9261  addmodlteq  9400  mulexpzap  9516  leexp1a  9531  expnbnd  9596  faclbnd  9668  cjap  9793  caucvgre  9867  cvg1nlemres  9871  resqrexlemglsq  9908  resqrexlemga  9909  sqrtsq  9930  ltabs  9973  abs3lem  9997  cau3lem  10000  maxleim  10091  rexico  10107  minmax  10112  climcau  10184  climrecvg1n  10185  dvdsle  10244  zsupcllemstep  10341  dvdsbnd  10348  gcdsupex  10349  gcdsupcl  10350  bezoutlemmain  10387  bezoutlemzz  10391  bezoutlembi  10394  dfgcd3  10399  dvdsmulgcd  10414  lcmcllem  10449  lcmgcdlem  10459  ncoprmgcdne1b  10471  pw2dvdslemn  10543  oddpwdclemxy  10547