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  6437  tfrlem1  6552  tfr1onlemaccex  6592  tfrcllemaccex  6605  frecabcl  6643  fopwdom  7102  phplem4dom  7129  phpm  7133  phplem4on  7135  fidifsnen  7138  diffisn  7163  diffifi  7164  en2eqpr  7180  fisseneq  7208  suplub2ti  7305  difinfsn  7404  ctmlemr  7412  ctm  7413  ctssdclemn0  7414  ctssdc  7417  nninfninc  7427  nninfisol  7437  enomnilem  7442  enmkvlem  7465  enwomnilem  7473  nninfwlpoimlemginf  7480  exmidontriimlem4  7544  exmidontriim  7545  cc3  7598  addcmpblnq  7698  mulcmpblnq  7699  ordpipqqs  7705  ltexnqq  7739  enq0tr  7765  addcmpblnq0  7774  mulcmpblnq0  7775  nnnq0lem1  7777  prssnqu  7811  prarloclemup  7826  nqprl  7882  nqpru  7883  mullocpr  7902  cauappcvgprlemladdfu  7985  cauappcvgprlemladdrl  7988  caucvgprlemm  7999  caucvgprlemladdfu  8008  caucvgprlemladdrl  8009  caucvgprlemlim  8012  caucvgprprlemml  8025  caucvgprprlemloc  8034  caucvgprprlemlim  8042  suplocexprlemmu  8049  suplocexprlemru  8050  suplocexprlemdisj  8051  suplocexprlemloc  8052  addcmpblnr  8070  mulcmpblnrlemg  8071  mulcmpblnr  8072  ltsrprg  8078  srpospr  8114  caucvgsrlemoffres  8131  suplocsrlemb  8137  suplocsrlempr  8138  suplocsrlem  8139  axcaucvglemcau  8229  axsuploc  8362  cnegexlem3  8466  negeu  8480  add20  8765  rimul  8876  apreap  8878  cru  8893  apreim  8894  apsym  8897  apcotr  8898  apadd1  8899  apneg  8902  mulext1  8903  apti  8913  aptap  8941  mulap0  8945  prodgt0  9143  ltmul12a  9151  ledivdiv  9181  lediv12a  9185  supinfneg  9945  infsupneg  9946  qapne  9989  xaddf  10196  xaddval  10197  xleadd1a  10225  xleaddadd  10239  ixxss12  10258  ioodisj  10345  fznlem  10395  zsupcllemstep  10611  qtri3or  10624  exbtwnzlemstep  10631  rebtwn2zlemstep  10636  addmodlteq  10784  seqf1og  10907  mulexpzap  10965  leexp1a  10980  expnbnd  11050  apexp1  11105  faclbnd  11128  hashxp  11216  sshashneg  11230  zfz1iso  11238  swrdswrdlem  11421  cjap  11616  caucvgre  11691  cvg1nlemres  11695  resqrexlemglsq  11732  resqrexlemga  11733  sqrtsq  11754  ltabs  11797  abs3lem  11821  cau3lem  11824  maxleim  11915  rexico  11931  minmax  11940  xrmaxleim  11954  xrmaxiflemcl  11955  xrmaxiflemlub  11958  xrmaxiflemval  11960  xrmaxltsup  11968  xrmaxadd  11971  xrminmax  11975  xrbdtri  11986  climcau  12057  climrecvg1n  12058  sumeq2  12069  summodclem2  12093  divcnv  12208  prodeq2  12268  fprodsplitdc  12307  fprodconst  12331  dvdsle  12555  bitsfzo  12666  dvdsbnd  12677  bezoutlemmain  12719  bezoutlemzz  12723  bezoutlembi  12726  dfgcd3  12731  dvdsmulgcd  12746  nnmindc  12755  lcmcllem  12789  lcmgcdlem  12799  ncoprmgcdne1b  12811  isprm5  12864  pw2dvdslemn  12887  oddpwdclemxy  12891  pythagtriplem2  12989  pythagtrip  13006  pceu  13018  pc2dvds  13053  pcz  13055  pcadd  13063  pcfac  13073  exmidunben  13261  ctiunctlemfo  13274  unct  13277  sgrppropd  13676  sgrpidmndm  13681  mndpropd  13701  mhmeql  13747  isgrpinv  13809  dfgrp3mlem  13853  mhmmnd  13869  conjnmzb  14033  ghmcmn  14080  gsumfzconst  14094  prdsval  14115  isrng  14173  issrg  14208  isring  14243  dvdsrmul1  14347  aprlring  14538  tgrest  15160  cnpnei  15210  cnss1  15217  cncnp  15221  ismet2  15345  metequiv2  15487  metcnp  15503  metcnp2  15504  metcnpi3  15508  fsumcncntop  15558  elcncf2  15565  cncfmet  15583  suplociccreex  15615  dedekindicclemicc  15623  ivthinclemlr  15628  ivthinclemur  15630  cnplimclemr  15660  limccnpcntop  15666  limccoap  15669  dvmptfsum  15716  elply2  15726  plyrecj  15754  mersenne  15991  lgsval2lem  16009  lgsquad3  16083  usgr1eop  16366  usgr1vr  16369  pw1ndom3  16890  nninfalllem1  16912  nnnninfex  16926  sbthom  16932  apdiff  16958  trimul0or  16971