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  6313  tfrlem1  6393  tfr1onlemaccex  6433  tfrcllemaccex  6446  frecabcl  6484  fopwdom  6932  phplem4dom  6958  phpm  6961  phplem4on  6963  fidifsnen  6966  diffisn  6989  diffifi  6990  en2eqpr  7003  fisseneq  7030  suplub2ti  7102  difinfsn  7201  ctmlemr  7209  ctm  7210  ctssdclemn0  7211  ctssdc  7214  nninfninc  7224  nninfisol  7234  enomnilem  7239  enmkvlem  7262  enwomnilem  7270  nninfwlpoimlemginf  7277  exmidontriimlem4  7335  exmidontriim  7336  cc3  7379  addcmpblnq  7479  mulcmpblnq  7480  ordpipqqs  7486  ltexnqq  7520  enq0tr  7546  addcmpblnq0  7555  mulcmpblnq0  7556  nnnq0lem1  7558  prssnqu  7592  prarloclemup  7607  nqprl  7663  nqpru  7664  mullocpr  7683  cauappcvgprlemladdfu  7766  cauappcvgprlemladdrl  7769  caucvgprlemm  7780  caucvgprlemladdfu  7789  caucvgprlemladdrl  7790  caucvgprlemlim  7793  caucvgprprlemml  7806  caucvgprprlemloc  7815  caucvgprprlemlim  7823  suplocexprlemmu  7830  suplocexprlemru  7831  suplocexprlemdisj  7832  suplocexprlemloc  7833  addcmpblnr  7851  mulcmpblnrlemg  7852  mulcmpblnr  7853  ltsrprg  7859  srpospr  7895  caucvgsrlemoffres  7912  suplocsrlemb  7918  suplocsrlempr  7919  suplocsrlem  7920  axcaucvglemcau  8010  axsuploc  8144  cnegexlem3  8248  negeu  8262  add20  8546  rimul  8657  apreap  8659  cru  8674  apreim  8675  apsym  8678  apcotr  8679  apadd1  8680  apneg  8683  mulext1  8684  apti  8694  aptap  8722  mulap0  8726  prodgt0  8924  ltmul12a  8932  ledivdiv  8962  lediv12a  8966  supinfneg  9715  infsupneg  9716  qapne  9759  xaddf  9965  xaddval  9966  xleadd1a  9994  xleaddadd  10008  ixxss12  10027  ioodisj  10114  fznlem  10162  zsupcllemstep  10370  qtri3or  10381  exbtwnzlemstep  10388  rebtwn2zlemstep  10393  addmodlteq  10541  seqf1og  10664  mulexpzap  10722  leexp1a  10737  expnbnd  10806  apexp1  10861  faclbnd  10884  hashxp  10969  zfz1iso  10984  cjap  11188  caucvgre  11263  cvg1nlemres  11267  resqrexlemglsq  11304  resqrexlemga  11305  sqrtsq  11326  ltabs  11369  abs3lem  11393  cau3lem  11396  maxleim  11487  rexico  11503  minmax  11512  xrmaxleim  11526  xrmaxiflemcl  11527  xrmaxiflemlub  11530  xrmaxiflemval  11532  xrmaxltsup  11540  xrmaxadd  11543  xrminmax  11547  xrbdtri  11558  climcau  11629  climrecvg1n  11630  sumeq2  11641  summodclem2  11664  divcnv  11779  prodeq2  11839  fprodsplitdc  11878  fprodconst  11902  dvdsle  12126  bitsfzo  12237  dvdsbnd  12248  bezoutlemmain  12290  bezoutlemzz  12294  bezoutlembi  12297  dfgcd3  12302  dvdsmulgcd  12317  nnmindc  12326  lcmcllem  12360  lcmgcdlem  12370  ncoprmgcdne1b  12382  isprm5  12435  pw2dvdslemn  12458  oddpwdclemxy  12462  pythagtriplem2  12560  pythagtrip  12577  pceu  12589  pc2dvds  12624  pcz  12626  pcadd  12634  pcfac  12644  exmidunben  12768  ctiunctlemfo  12781  unct  12784  prdsval  13076  sgrppropd  13216  sgrpidmndm  13223  mndpropd  13243  mhmeql  13295  isgrpinv  13357  dfgrp3mlem  13401  mhmmnd  13423  conjnmzb  13587  ghmcmn  13634  gsumfzconst  13648  isrng  13667  issrg  13698  isring  13733  reldvdsrsrg  13825  dvdsrmul1  13835  tgrest  14612  cnpnei  14662  cnss1  14669  cncnp  14673  ismet2  14797  metequiv2  14939  metcnp  14955  metcnp2  14956  metcnpi3  14960  fsumcncntop  15010  elcncf2  15017  cncfmet  15035  suplociccreex  15067  dedekindicclemicc  15075  ivthinclemlr  15080  ivthinclemur  15082  cnplimclemr  15112  limccnpcntop  15118  limccoap  15121  dvmptfsum  15168  elply2  15178  plyrecj  15206  mersenne  15440  lgsval2lem  15458  lgsquad3  15532  nninfalllem1  15907  nnnninfex  15921  sbthom  15927  apdiff  15949