Theorem simpllr 540

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 492	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  548  f1o2ndf1  6454  tfrlem1  6569  tfr1onlemaccex  6609  tfrcllemaccex  6622  frecabcl  6660  fopwdom  7126  phplem4dom  7153  phpm  7157  phplem4on  7159  fidifsnen  7162  diffisn  7187  diffifi  7188  en2eqpr  7204  fisseneq  7232  suplub2ti  7331  difinfsn  7430  ctmlemr  7438  ctm  7439  ctssdclemn0  7440  ctssdc  7443  nninfninc  7453  nninfisol  7463  enomnilem  7468  enmkvlem  7491  enwomnilem  7499  nninfwlpoimlemginf  7506  exmidontriimlem4  7570  exmidontriim  7571  cc3  7624  addcmpblnq  7724  mulcmpblnq  7725  ordpipqqs  7731  ltexnqq  7765  enq0tr  7791  addcmpblnq0  7800  mulcmpblnq0  7801  nnnq0lem1  7803  prssnqu  7837  prarloclemup  7852  nqprl  7908  nqpru  7909  mullocpr  7928  cauappcvgprlemladdfu  8011  cauappcvgprlemladdrl  8014  caucvgprlemm  8025  caucvgprlemladdfu  8034  caucvgprlemladdrl  8035  caucvgprlemlim  8038  caucvgprprlemml  8051  caucvgprprlemloc  8060  caucvgprprlemlim  8068  suplocexprlemmu  8075  suplocexprlemru  8076  suplocexprlemdisj  8077  suplocexprlemloc  8078  addcmpblnr  8096  mulcmpblnrlemg  8097  mulcmpblnr  8098  ltsrprg  8104  srpospr  8140  caucvgsrlemoffres  8157  suplocsrlemb  8163  suplocsrlempr  8164  suplocsrlem  8165  axcaucvglemcau  8255  axsuploc  8388  cnegexlem3  8493  negeu  8507  add20  8792  rimul  8903  apreap  8905  cru  8920  apreim  8921  apsym  8924  apcotr  8925  apadd1  8926  apneg  8929  mulext1  8930  apti  8940  aptap  8968  mulap0  8972  prodgt0  9172  ltmul12a  9180  ledivdiv  9210  lediv12a  9214  supinfneg  9974  infsupneg  9975  qapne  10018  xaddf  10225  xaddval  10226  xleadd1a  10254  xleaddadd  10268  ixxss12  10287  ioodisj  10374  fznlem  10424  zsupcllemstep  10640  qtri3or  10653  exbtwnzlemstep  10660  rebtwn2zlemstep  10665  addmodlteq  10813  seqf1og  10936  mulexpzap  10994  leexp1a  11009  expnbnd  11079  apexp1  11134  faclbnd  11157  hashxp  11245  sshashneg  11259  hashf1lem2  11264  zfz1iso  11271  swrdswrdlem  11454  cjap  11650  caucvgre  11725  cvg1nlemres  11729  resqrexlemglsq  11766  resqrexlemga  11767  sqrtsq  11788  ltabs  11831  abs3lem  11855  cau3lem  11858  maxleim  11949  rexico  11965  minmax  11974  xrmaxleim  11988  xrmaxiflemcl  11989  xrmaxiflemlub  11992  xrmaxiflemval  11994  xrmaxltsup  12002  xrmaxadd  12005  xrminmax  12009  xrbdtri  12020  climcau  12091  climrecvg1n  12092  sumeq2  12103  summodclem2  12127  divcnv  12242  prodeq2  12302  fprodsplitdc  12341  fprodconst  12365  dvdsle  12589  bitsfzo  12700  dvdsbnd  12711  bezoutlemmain  12753  bezoutlemzz  12757  bezoutlembi  12760  dfgcd3  12765  dvdsmulgcd  12780  nnmindc  12789  lcmcllem  12823  lcmgcdlem  12833  ncoprmgcdne1b  12845  isprm5  12898  pw2dvdslemn  12921  oddpwdclemxy  12925  pythagtriplem2  13023  pythagtrip  13040  pceu  13052  pc2dvds  13087  pcz  13089  pcadd  13097  pcfac  13107  exmidunben  13295  ctiunctlemfo  13308  unct  13311  sgrppropd  13705  sgrpidmndm  13710  mndpropd  13730  mhmeql  13776  isgrpinv  13836  dfgrp3mlem  13880  mhmmnd  13896  conjnmzb  14060  ghmcmn  14108  gzsumconst  14120  prdsval  14150  isrng  14208  issrg  14243  isring  14278  dvdsrmul1  14382  aprlring  14573  tgrest  15193  cnpnei  15243  cnss1  15250  cncnp  15254  ismet2  15378  metequiv2  15520  metcnp  15536  metcnp2  15537  metcnpi3  15541  fsumcncntop  15591  elcncf2  15598  cncfmet  15616  suplociccreex  15648  dedekindicclemicc  15656  ivthinclemlr  15661  ivthinclemur  15663  cnplimclemr  15693  limccnpcntop  15699  limccoap  15702  dvmptfsum  15749  elply2  15759  plyrecj  15787  mersenne  16025  lgsval2lem  16043  lgsquad3  16117  usgr1eop  16400  usgr1vr  16403  pw1ndom3  16934  nninfalllem1  16956  nnnninfex  16970  sbthom  16976  apdiff  17002