Theorem simpllr 536

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  simp-4r  544  f1o2ndf1  6423  tfrlem1  6538  tfr1onlemaccex  6578  tfrcllemaccex  6591  frecabcl  6629  fopwdom  7088  phplem4dom  7115  phpm  7119  phplem4on  7121  fidifsnen  7124  diffisn  7149  diffifi  7150  en2eqpr  7166  fisseneq  7194  suplub2ti  7291  difinfsn  7390  ctmlemr  7398  ctm  7399  ctssdclemn0  7400  ctssdc  7403  nninfninc  7413  nninfisol  7423  enomnilem  7428  enmkvlem  7451  enwomnilem  7459  nninfwlpoimlemginf  7466  exmidontriimlem4  7530  exmidontriim  7531  cc3  7581  addcmpblnq  7681  mulcmpblnq  7682  ordpipqqs  7688  ltexnqq  7722  enq0tr  7748  addcmpblnq0  7757  mulcmpblnq0  7758  nnnq0lem1  7760  prssnqu  7794  prarloclemup  7809  nqprl  7865  nqpru  7866  mullocpr  7885  cauappcvgprlemladdfu  7968  cauappcvgprlemladdrl  7971  caucvgprlemm  7982  caucvgprlemladdfu  7991  caucvgprlemladdrl  7992  caucvgprlemlim  7995  caucvgprprlemml  8008  caucvgprprlemloc  8017  caucvgprprlemlim  8025  suplocexprlemmu  8032  suplocexprlemru  8033  suplocexprlemdisj  8034  suplocexprlemloc  8035  addcmpblnr  8053  mulcmpblnrlemg  8054  mulcmpblnr  8055  ltsrprg  8061  srpospr  8097  caucvgsrlemoffres  8114  suplocsrlemb  8120  suplocsrlempr  8121  suplocsrlem  8122  axcaucvglemcau  8212  axsuploc  8345  cnegexlem3  8449  negeu  8463  add20  8747  rimul  8858  apreap  8860  cru  8875  apreim  8876  apsym  8879  apcotr  8880  apadd1  8881  apneg  8884  mulext1  8885  apti  8895  aptap  8923  mulap0  8927  prodgt0  9125  ltmul12a  9133  ledivdiv  9163  lediv12a  9167  supinfneg  9926  infsupneg  9927  qapne  9970  xaddf  10176  xaddval  10177  xleadd1a  10205  xleaddadd  10219  ixxss12  10238  ioodisj  10325  fznlem  10374  zsupcllemstep  10588  qtri3or  10599  exbtwnzlemstep  10606  rebtwn2zlemstep  10611  addmodlteq  10759  seqf1og  10882  mulexpzap  10940  leexp1a  10955  expnbnd  11024  apexp1  11079  faclbnd  11102  hashxp  11189  sshashneg  11201  zfz1iso  11209  swrdswrdlem  11392  cjap  11587  caucvgre  11662  cvg1nlemres  11666  resqrexlemglsq  11703  resqrexlemga  11704  sqrtsq  11725  ltabs  11768  abs3lem  11792  cau3lem  11795  maxleim  11886  rexico  11902  minmax  11911  xrmaxleim  11925  xrmaxiflemcl  11926  xrmaxiflemlub  11929  xrmaxiflemval  11931  xrmaxltsup  11939  xrmaxadd  11942  xrminmax  11946  xrbdtri  11957  climcau  12028  climrecvg1n  12029  sumeq2  12040  summodclem2  12064  divcnv  12179  prodeq2  12239  fprodsplitdc  12278  fprodconst  12302  dvdsle  12526  bitsfzo  12637  dvdsbnd  12648  bezoutlemmain  12690  bezoutlemzz  12694  bezoutlembi  12697  dfgcd3  12702  dvdsmulgcd  12717  nnmindc  12726  lcmcllem  12760  lcmgcdlem  12770  ncoprmgcdne1b  12782  isprm5  12835  pw2dvdslemn  12858  oddpwdclemxy  12862  pythagtriplem2  12960  pythagtrip  12977  pceu  12989  pc2dvds  13024  pcz  13026  pcadd  13034  pcfac  13044  exmidunben  13169  ctiunctlemfo  13182  unct  13185  prdsval  13478  sgrppropd  13618  sgrpidmndm  13625  mndpropd  13645  mhmeql  13697  isgrpinv  13759  dfgrp3mlem  13803  mhmmnd  13825  conjnmzb  13989  ghmcmn  14036  gsumfzconst  14050  isrng  14070  issrg  14101  isring  14136  dvdsrmul1  14239  aprlring  14426  tgrest  15026  cnpnei  15076  cnss1  15083  cncnp  15087  ismet2  15211  metequiv2  15353  metcnp  15369  metcnp2  15370  metcnpi3  15374  fsumcncntop  15424  elcncf2  15431  cncfmet  15449  suplociccreex  15481  dedekindicclemicc  15489  ivthinclemlr  15494  ivthinclemur  15496  cnplimclemr  15526  limccnpcntop  15532  limccoap  15535  dvmptfsum  15582  elply2  15592  plyrecj  15620  mersenne  15857  lgsval2lem  15875  lgsquad3  15949  usgr1eop  16232  usgr1vr  16235  pw1ndom3  16756  nninfalllem1  16778  nnnninfex  16792  sbthom  16798  apdiff  16824