Theorem simpllr 529

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 485	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  537  f1o2ndf1  6207  tfrlem1  6287  tfr1onlemaccex  6327  tfrcllemaccex  6340  frecabcl  6378  fopwdom  6814  phplem4dom  6840  phpm  6843  phplem4on  6845  fidifsnen  6848  diffisn  6871  diffifi  6872  en2eqpr  6885  fisseneq  6909  suplub2ti  6978  difinfsn  7077  ctmlemr  7085  ctm  7086  ctssdclemn0  7087  ctssdc  7090  nninfisol  7109  enomnilem  7114  enmkvlem  7137  enwomnilem  7145  nninfwlpoimlemginf  7152  exmidontriimlem4  7201  exmidontriim  7202  cc3  7230  addcmpblnq  7329  mulcmpblnq  7330  ordpipqqs  7336  ltexnqq  7370  enq0tr  7396  addcmpblnq0  7405  mulcmpblnq0  7406  nnnq0lem1  7408  prssnqu  7442  prarloclemup  7457  nqprl  7513  nqpru  7514  mullocpr  7533  cauappcvgprlemladdfu  7616  cauappcvgprlemladdrl  7619  caucvgprlemm  7630  caucvgprlemladdfu  7639  caucvgprlemladdrl  7640  caucvgprlemlim  7643  caucvgprprlemml  7656  caucvgprprlemloc  7665  caucvgprprlemlim  7673  suplocexprlemmu  7680  suplocexprlemru  7681  suplocexprlemdisj  7682  suplocexprlemloc  7683  addcmpblnr  7701  mulcmpblnrlemg  7702  mulcmpblnr  7703  ltsrprg  7709  srpospr  7745  caucvgsrlemoffres  7762  suplocsrlemb  7768  suplocsrlempr  7769  suplocsrlem  7770  axcaucvglemcau  7860  axsuploc  7992  cnegexlem3  8096  negeu  8110  add20  8393  rimul  8504  apreap  8506  cru  8521  apreim  8522  apsym  8525  apcotr  8526  apadd1  8527  apneg  8530  mulext1  8531  apti  8541  mulap0  8572  prodgt0  8768  ltmul12a  8776  ledivdiv  8806  lediv12a  8810  supinfneg  9554  infsupneg  9555  qapne  9598  xaddf  9801  xaddval  9802  xleadd1a  9830  xleaddadd  9844  ixxss12  9863  ioodisj  9950  fznlem  9997  qtri3or  10199  exbtwnzlemstep  10204  rebtwn2zlemstep  10209  addmodlteq  10354  mulexpzap  10516  leexp1a  10531  expnbnd  10599  apexp1  10652  faclbnd  10675  hashxp  10761  zfz1iso  10776  cjap  10870  caucvgre  10945  cvg1nlemres  10949  resqrexlemglsq  10986  resqrexlemga  10987  sqrtsq  11008  ltabs  11051  abs3lem  11075  cau3lem  11078  maxleim  11169  rexico  11185  minmax  11193  xrmaxleim  11207  xrmaxiflemcl  11208  xrmaxiflemlub  11211  xrmaxiflemval  11213  xrmaxltsup  11221  xrmaxadd  11224  xrminmax  11228  xrbdtri  11239  climcau  11310  climrecvg1n  11311  sumeq2  11322  summodclem2  11345  divcnv  11460  prodeq2  11520  fprodsplitdc  11559  fprodconst  11583  dvdsle  11804  zsupcllemstep  11900  dvdsbnd  11911  gcdsupex  11912  gcdsupcl  11913  bezoutlemmain  11953  bezoutlemzz  11957  bezoutlembi  11960  dfgcd3  11965  dvdsmulgcd  11980  nnmindc  11989  lcmcllem  12021  lcmgcdlem  12031  ncoprmgcdne1b  12043  isprm5  12096  pw2dvdslemn  12119  oddpwdclemxy  12123  pythagtriplem2  12220  pythagtrip  12237  pceu  12249  pc2dvds  12283  pcz  12285  pcadd  12293  pcfac  12302  exmidunben  12381  ctiunctlemfo  12394  unct  12397  sgrpidmndm  12656  mndpropd  12676  mhmeql  12707  isgrpinv  12756  tgrest  12963  cnpnei  13013  cnss1  13020  cncnp  13024  ismet2  13148  metequiv2  13290  metcnp  13306  metcnp2  13307  metcnpi3  13311  fsumcncntop  13350  elcncf2  13355  cncfmet  13373  suplociccreex  13396  dedekindicclemicc  13404  ivthinclemlr  13409  ivthinclemur  13411  cnplimclemr  13432  limccnpcntop  13438  limccoap  13441  lgsval2lem  13705  nninfalllem1  14041  sbthom  14058  apdiff  14080