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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  simp-4r  548  f1o2ndf1  6464  tfrlem1  6579  tfr1onlemaccex  6619  tfrcllemaccex  6632  frecabcl  6670  fopwdom  7136  phplem4dom  7163  phpm  7167  phplem4on  7169  fidifsnen  7172  diffisn  7197  diffifi  7198  en2eqpr  7214  fisseneq  7242  suplub2ti  7341  difinfsn  7440  ctmlemr  7448  ctm  7449  ctssdclemn0  7450  ctssdc  7453  nninfninc  7463  nninfisol  7473  enomnilem  7478  enmkvlem  7501  enwomnilem  7509  nninfwlpoimlemginf  7516  exmidontriimlem4  7580  exmidontriim  7581  cc3  7634  addcmpblnq  7734  mulcmpblnq  7735  ordpipqqs  7741  ltexnqq  7775  enq0tr  7801  addcmpblnq0  7810  mulcmpblnq0  7811  nnnq0lem1  7813  prssnqu  7847  prarloclemup  7862  nqprl  7918  nqpru  7919  mullocpr  7938  cauappcvgprlemladdfu  8021  cauappcvgprlemladdrl  8024  caucvgprlemm  8035  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  caucvgprlemlim  8048  caucvgprprlemml  8061  caucvgprprlemloc  8070  caucvgprprlemlim  8078  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  addcmpblnr  8106  mulcmpblnrlemg  8107  mulcmpblnr  8108  ltsrprg  8114  srpospr  8150  caucvgsrlemoffres  8167  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  axcaucvglemcau  8265  axsuploc  8398  cnegexlem3  8504  negeu  8518  add20  8803  rimul  8915  apreap  8917  cru  8932  apreim  8933  apsym  8936  apcotr  8937  apadd1  8938  apneg  8941  mulext1  8942  apti  8952  aptap  8980  mulap0  8984  prodgt0  9184  ltmul12a  9192  ledivdiv  9222  lediv12a  9226  supinfneg  10004  infsupneg  10005  qapne  10048  irraddap  10056  xaddf  10256  xaddval  10257  xleadd1a  10285  xleaddadd  10299  ixxss12  10318  ioodisj  10405  fznlem  10455  zsupcllemstep  10672  qtri3or  10685  exbtwnzlemstep  10692  rebtwn2zlemstep  10697  addmodlteq  10848  seqf1og  10971  mulexpzap  11029  leexp1a  11044  expnbnd  11114  apexp1  11170  faclbnd  11193  hashxp  11281  sshashneg  11295  hashf1lem2  11300  zfz1iso  11307  swrdswrdlem  11490  cjap  11686  caucvgre  11761  cvg1nlemres  11765  resqrexlemglsq  11802  resqrexlemga  11803  sqrtsq  11824  ltabs  11868  abs3lem  11892  cau3lem  11895  maxleim  11986  rexico  12002  minmax  12011  xrmaxleim  12026  xrmaxiflemcl  12027  xrmaxiflemlub  12030  xrmaxiflemval  12032  xrmaxltsup  12040  xrmaxadd  12043  xrminmax  12047  xrbdtri  12058  climcau  12129  climrecvg1n  12130  sumeq2  12141  summodclem2  12165  divcnv  12280  prodeq2  12340  fprodsplitdc  12379  fprodconst  12403  dvdsle  12627  bitsfzo  12738  dvdsbnd  12749  bezoutlemmain  12791  bezoutlemzz  12795  bezoutlembi  12798  dfgcd3  12803  dvdsmulgcd  12818  nnmindc  12827  lcmcllem  12861  lcmgcdlem  12871  ncoprmgcdne1b  12883  isprm5  12937  pwbdvdslemn  12960  nnmaxpwlemparts  12968  pythagtriplem2  13065  pythagtrip  13082  pceu  13094  pc2dvds  13129  pcz  13131  pcadd  13139  pcfac  13149  exmidunben  13366  ctiunctlemfo  13379  unct  13382  sgrppropd  13777  sgrpidmndm  13782  mndpropd  13802  mhmeql  13848  isgrpinv  13908  dfgrp3mlem  13952  mhmmnd  13968  conjnmzb  14132  ghmcmn  14180  gzsumconst  14192  prdsval  14222  isrng  14282  issrg  14318  isring  14353  dvdsrmul1  14458  aprlring  14649  issubassa2  15084  tgrest  15319  cnpnei  15369  cnss1  15376  cncnp  15380  ismet2  15504  metequiv2  15646  metcnp  15662  metcnp2  15663  metcnpi3  15667  fsumcncntop  15717  elcncf2  15724  cncfmet  15742  suplociccreex  15774  dedekindicclemicc  15782  ivthinclemlr  15787  ivthinclemur  15789  cnplimclemr  15819  limccnpcntop  15825  limccoap  15828  dvmptfsum  15875  elply2  15885  plyrecj  15913  logdivlt  16046  zprmlogbap  16137  mersenne  16195  lgsval2lem  16227  lgsquad3  16301  usgr1eop  16584  usgr1vr  16587  pw1ndom3  17118  nninfalllem1  17149  nnnninfex  17163  sbthom  17169  apdiff  17195