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  8503  negeu  8517  add20  8802  rimul  8913  apreap  8915  cru  8930  apreim  8931  apsym  8934  apcotr  8935  apadd1  8936  apneg  8939  mulext1  8940  apti  8950  aptap  8978  mulap0  8982  prodgt0  9182  ltmul12a  9190  ledivdiv  9220  lediv12a  9224  supinfneg  9995  infsupneg  9996  qapne  10039  xaddf  10246  xaddval  10247  xleadd1a  10275  xleaddadd  10289  ixxss12  10308  ioodisj  10395  fznlem  10445  zsupcllemstep  10662  qtri3or  10675  exbtwnzlemstep  10682  rebtwn2zlemstep  10687  addmodlteq  10835  seqf1og  10958  mulexpzap  11016  leexp1a  11031  expnbnd  11101  apexp1  11156  faclbnd  11179  hashxp  11267  sshashneg  11281  hashf1lem2  11286  zfz1iso  11293  swrdswrdlem  11476  cjap  11672  caucvgre  11747  cvg1nlemres  11751  resqrexlemglsq  11788  resqrexlemga  11789  sqrtsq  11810  ltabs  11853  abs3lem  11877  cau3lem  11880  maxleim  11971  rexico  11987  minmax  11996  xrmaxleim  12010  xrmaxiflemcl  12011  xrmaxiflemlub  12014  xrmaxiflemval  12016  xrmaxltsup  12024  xrmaxadd  12027  xrminmax  12031  xrbdtri  12042  climcau  12113  climrecvg1n  12114  sumeq2  12125  summodclem2  12149  divcnv  12264  prodeq2  12324  fprodsplitdc  12363  fprodconst  12387  dvdsle  12611  bitsfzo  12722  dvdsbnd  12733  bezoutlemmain  12775  bezoutlemzz  12779  bezoutlembi  12782  dfgcd3  12787  dvdsmulgcd  12802  nnmindc  12811  lcmcllem  12845  lcmgcdlem  12855  ncoprmgcdne1b  12867  isprm5  12920  pw2dvdslemn  12943  oddpwdclemxy  12947  pythagtriplem2  13045  pythagtrip  13062  pceu  13074  pc2dvds  13109  pcz  13111  pcadd  13119  pcfac  13129  exmidunben  13317  ctiunctlemfo  13330  unct  13333  sgrppropd  13728  sgrpidmndm  13733  mndpropd  13753  mhmeql  13799  isgrpinv  13859  dfgrp3mlem  13903  mhmmnd  13919  conjnmzb  14083  ghmcmn  14131  gzsumconst  14143  prdsval  14173  isrng  14233  issrg  14269  isring  14304  dvdsrmul1  14409  aprlring  14600  issubassa2  15035  tgrest  15270  cnpnei  15320  cnss1  15327  cncnp  15331  ismet2  15455  metequiv2  15597  metcnp  15613  metcnp2  15614  metcnpi3  15618  fsumcncntop  15668  elcncf2  15675  cncfmet  15693  suplociccreex  15725  dedekindicclemicc  15733  ivthinclemlr  15738  ivthinclemur  15740  cnplimclemr  15770  limccnpcntop  15776  limccoap  15779  dvmptfsum  15826  elply2  15836  plyrecj  15864  mersenne  16111  lgsval2lem  16129  lgsquad3  16203  usgr1eop  16486  usgr1vr  16489  pw1ndom3  17020  nninfalllem1  17051  nnnninfex  17065  sbthom  17071  apdiff  17097