Theorem simpllr 534

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  542  f1o2ndf1  6388  tfrlem1  6469  tfr1onlemaccex  6509  tfrcllemaccex  6522  frecabcl  6560  fopwdom  7017  phplem4dom  7043  phpm  7047  phplem4on  7049  fidifsnen  7052  diffisn  7075  diffifi  7076  en2eqpr  7092  fisseneq  7119  suplub2ti  7191  difinfsn  7290  ctmlemr  7298  ctm  7299  ctssdclemn0  7300  ctssdc  7303  nninfninc  7313  nninfisol  7323  enomnilem  7328  enmkvlem  7351  enwomnilem  7359  nninfwlpoimlemginf  7366  exmidontriimlem4  7429  exmidontriim  7430  cc3  7477  addcmpblnq  7577  mulcmpblnq  7578  ordpipqqs  7584  ltexnqq  7618  enq0tr  7644  addcmpblnq0  7653  mulcmpblnq0  7654  nnnq0lem1  7656  prssnqu  7690  prarloclemup  7705  nqprl  7761  nqpru  7762  mullocpr  7781  cauappcvgprlemladdfu  7864  cauappcvgprlemladdrl  7867  caucvgprlemm  7878  caucvgprlemladdfu  7887  caucvgprlemladdrl  7888  caucvgprlemlim  7891  caucvgprprlemml  7904  caucvgprprlemloc  7913  caucvgprprlemlim  7921  suplocexprlemmu  7928  suplocexprlemru  7929  suplocexprlemdisj  7930  suplocexprlemloc  7931  addcmpblnr  7949  mulcmpblnrlemg  7950  mulcmpblnr  7951  ltsrprg  7957  srpospr  7993  caucvgsrlemoffres  8010  suplocsrlemb  8016  suplocsrlempr  8017  suplocsrlem  8018  axcaucvglemcau  8108  axsuploc  8242  cnegexlem3  8346  negeu  8360  add20  8644  rimul  8755  apreap  8757  cru  8772  apreim  8773  apsym  8776  apcotr  8777  apadd1  8778  apneg  8781  mulext1  8782  apti  8792  aptap  8820  mulap0  8824  prodgt0  9022  ltmul12a  9030  ledivdiv  9060  lediv12a  9064  supinfneg  9819  infsupneg  9820  qapne  9863  xaddf  10069  xaddval  10070  xleadd1a  10098  xleaddadd  10112  ixxss12  10131  ioodisj  10218  fznlem  10266  zsupcllemstep  10479  qtri3or  10490  exbtwnzlemstep  10497  rebtwn2zlemstep  10502  addmodlteq  10650  seqf1og  10773  mulexpzap  10831  leexp1a  10846  expnbnd  10915  apexp1  10970  faclbnd  10993  hashxp  11080  zfz1iso  11095  swrdswrdlem  11275  cjap  11457  caucvgre  11532  cvg1nlemres  11536  resqrexlemglsq  11573  resqrexlemga  11574  sqrtsq  11595  ltabs  11638  abs3lem  11662  cau3lem  11665  maxleim  11756  rexico  11772  minmax  11781  xrmaxleim  11795  xrmaxiflemcl  11796  xrmaxiflemlub  11799  xrmaxiflemval  11801  xrmaxltsup  11809  xrmaxadd  11812  xrminmax  11816  xrbdtri  11827  climcau  11898  climrecvg1n  11899  sumeq2  11910  summodclem2  11933  divcnv  12048  prodeq2  12108  fprodsplitdc  12147  fprodconst  12171  dvdsle  12395  bitsfzo  12506  dvdsbnd  12517  bezoutlemmain  12559  bezoutlemzz  12563  bezoutlembi  12566  dfgcd3  12571  dvdsmulgcd  12586  nnmindc  12595  lcmcllem  12629  lcmgcdlem  12639  ncoprmgcdne1b  12651  isprm5  12704  pw2dvdslemn  12727  oddpwdclemxy  12731  pythagtriplem2  12829  pythagtrip  12846  pceu  12858  pc2dvds  12893  pcz  12895  pcadd  12903  pcfac  12913  exmidunben  13037  ctiunctlemfo  13050  unct  13053  prdsval  13346  sgrppropd  13486  sgrpidmndm  13493  mndpropd  13513  mhmeql  13565  isgrpinv  13627  dfgrp3mlem  13671  mhmmnd  13693  conjnmzb  13857  ghmcmn  13904  gsumfzconst  13918  isrng  13937  issrg  13968  isring  14003  dvdsrmul1  14106  tgrest  14883  cnpnei  14933  cnss1  14940  cncnp  14944  ismet2  15068  metequiv2  15210  metcnp  15226  metcnp2  15227  metcnpi3  15231  fsumcncntop  15281  elcncf2  15288  cncfmet  15306  suplociccreex  15338  dedekindicclemicc  15346  ivthinclemlr  15351  ivthinclemur  15353  cnplimclemr  15383  limccnpcntop  15389  limccoap  15392  dvmptfsum  15439  elply2  15449  plyrecj  15477  mersenne  15711  lgsval2lem  15729  lgsquad3  15803  usgr1eop  16084  usgr1vr  16087  pw1ndom3  16525  nninfalllem1  16546  nnnninfex  16560  sbthom  16566  apdiff  16588