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  6192  tfrlem1  6272  tfr1onlemaccex  6312  tfrcllemaccex  6325  frecabcl  6363  fopwdom  6798  phplem4dom  6824  phpm  6827  phplem4on  6829  fidifsnen  6832  diffisn  6855  diffifi  6856  en2eqpr  6869  fisseneq  6893  suplub2ti  6962  difinfsn  7061  ctmlemr  7069  ctm  7070  ctssdclemn0  7071  ctssdc  7074  nninfisol  7093  enomnilem  7098  enmkvlem  7121  enwomnilem  7129  exmidontriimlem4  7176  exmidontriim  7177  cc3  7205  addcmpblnq  7304  mulcmpblnq  7305  ordpipqqs  7311  ltexnqq  7345  enq0tr  7371  addcmpblnq0  7380  mulcmpblnq0  7381  nnnq0lem1  7383  prssnqu  7417  prarloclemup  7432  nqprl  7488  nqpru  7489  mullocpr  7508  cauappcvgprlemladdfu  7591  cauappcvgprlemladdrl  7594  caucvgprlemm  7605  caucvgprlemladdfu  7614  caucvgprlemladdrl  7615  caucvgprlemlim  7618  caucvgprprlemml  7631  caucvgprprlemloc  7640  caucvgprprlemlim  7648  suplocexprlemmu  7655  suplocexprlemru  7656  suplocexprlemdisj  7657  suplocexprlemloc  7658  addcmpblnr  7676  mulcmpblnrlemg  7677  mulcmpblnr  7678  ltsrprg  7684  srpospr  7720  caucvgsrlemoffres  7737  suplocsrlemb  7743  suplocsrlempr  7744  suplocsrlem  7745  axcaucvglemcau  7835  axsuploc  7967  cnegexlem3  8071  negeu  8085  add20  8368  rimul  8479  apreap  8481  cru  8496  apreim  8497  apsym  8500  apcotr  8501  apadd1  8502  apneg  8505  mulext1  8506  apti  8516  mulap0  8547  prodgt0  8743  ltmul12a  8751  ledivdiv  8781  lediv12a  8785  supinfneg  9529  infsupneg  9530  qapne  9573  xaddf  9776  xaddval  9777  xleadd1a  9805  xleaddadd  9819  ixxss12  9838  ioodisj  9925  fznlem  9972  qtri3or  10174  exbtwnzlemstep  10179  rebtwn2zlemstep  10184  addmodlteq  10329  mulexpzap  10491  leexp1a  10506  expnbnd  10574  apexp1  10627  faclbnd  10650  hashxp  10735  zfz1iso  10750  cjap  10844  caucvgre  10919  cvg1nlemres  10923  resqrexlemglsq  10960  resqrexlemga  10961  sqrtsq  10982  ltabs  11025  abs3lem  11049  cau3lem  11052  maxleim  11143  rexico  11159  minmax  11167  xrmaxleim  11181  xrmaxiflemcl  11182  xrmaxiflemlub  11185  xrmaxiflemval  11187  xrmaxltsup  11195  xrmaxadd  11198  xrminmax  11202  xrbdtri  11213  climcau  11284  climrecvg1n  11285  sumeq2  11296  summodclem2  11319  divcnv  11434  prodeq2  11494  fprodsplitdc  11533  fprodconst  11557  dvdsle  11778  zsupcllemstep  11874  dvdsbnd  11885  gcdsupex  11886  gcdsupcl  11887  bezoutlemmain  11927  bezoutlemzz  11931  bezoutlembi  11934  dfgcd3  11939  dvdsmulgcd  11954  nnmindc  11963  lcmcllem  11995  lcmgcdlem  12005  ncoprmgcdne1b  12017  isprm5  12070  pw2dvdslemn  12093  oddpwdclemxy  12097  pythagtriplem2  12194  pythagtrip  12211  pceu  12223  pc2dvds  12257  pcz  12259  pcadd  12267  pcfac  12276  exmidunben  12355  ctiunctlemfo  12368  unct  12371  tgrest  12769  cnpnei  12819  cnss1  12826  cncnp  12830  ismet2  12954  metequiv2  13096  metcnp  13112  metcnp2  13113  metcnpi3  13117  fsumcncntop  13156  elcncf2  13161  cncfmet  13179  suplociccreex  13202  dedekindicclemicc  13210  ivthinclemlr  13215  ivthinclemur  13217  cnplimclemr  13238  limccnpcntop  13244  limccoap  13247  lgsval2lem  13511  nninfalllem1  13848  sbthom  13865  apdiff  13887