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  6332  tfrlem1  6412  tfr1onlemaccex  6452  tfrcllemaccex  6465  frecabcl  6503  fopwdom  6953  phplem4dom  6979  phpm  6983  phplem4on  6985  fidifsnen  6988  diffisn  7011  diffifi  7012  en2eqpr  7025  fisseneq  7052  suplub2ti  7124  difinfsn  7223  ctmlemr  7231  ctm  7232  ctssdclemn0  7233  ctssdc  7236  nninfninc  7246  nninfisol  7256  enomnilem  7261  enmkvlem  7284  enwomnilem  7292  nninfwlpoimlemginf  7299  exmidontriimlem4  7362  exmidontriim  7363  cc3  7410  addcmpblnq  7510  mulcmpblnq  7511  ordpipqqs  7517  ltexnqq  7551  enq0tr  7577  addcmpblnq0  7586  mulcmpblnq0  7587  nnnq0lem1  7589  prssnqu  7623  prarloclemup  7638  nqprl  7694  nqpru  7695  mullocpr  7714  cauappcvgprlemladdfu  7797  cauappcvgprlemladdrl  7800  caucvgprlemm  7811  caucvgprlemladdfu  7820  caucvgprlemladdrl  7821  caucvgprlemlim  7824  caucvgprprlemml  7837  caucvgprprlemloc  7846  caucvgprprlemlim  7854  suplocexprlemmu  7861  suplocexprlemru  7862  suplocexprlemdisj  7863  suplocexprlemloc  7864  addcmpblnr  7882  mulcmpblnrlemg  7883  mulcmpblnr  7884  ltsrprg  7890  srpospr  7926  caucvgsrlemoffres  7943  suplocsrlemb  7949  suplocsrlempr  7950  suplocsrlem  7951  axcaucvglemcau  8041  axsuploc  8175  cnegexlem3  8279  negeu  8293  add20  8577  rimul  8688  apreap  8690  cru  8705  apreim  8706  apsym  8709  apcotr  8710  apadd1  8711  apneg  8714  mulext1  8715  apti  8725  aptap  8753  mulap0  8757  prodgt0  8955  ltmul12a  8963  ledivdiv  8993  lediv12a  8997  supinfneg  9746  infsupneg  9747  qapne  9790  xaddf  9996  xaddval  9997  xleadd1a  10025  xleaddadd  10039  ixxss12  10058  ioodisj  10145  fznlem  10193  zsupcllemstep  10404  qtri3or  10415  exbtwnzlemstep  10422  rebtwn2zlemstep  10427  addmodlteq  10575  seqf1og  10698  mulexpzap  10756  leexp1a  10771  expnbnd  10840  apexp1  10895  faclbnd  10918  hashxp  11003  zfz1iso  11018  swrdswrdlem  11190  cjap  11302  caucvgre  11377  cvg1nlemres  11381  resqrexlemglsq  11418  resqrexlemga  11419  sqrtsq  11440  ltabs  11483  abs3lem  11507  cau3lem  11510  maxleim  11601  rexico  11617  minmax  11626  xrmaxleim  11640  xrmaxiflemcl  11641  xrmaxiflemlub  11644  xrmaxiflemval  11646  xrmaxltsup  11654  xrmaxadd  11657  xrminmax  11661  xrbdtri  11672  climcau  11743  climrecvg1n  11744  sumeq2  11755  summodclem2  11778  divcnv  11893  prodeq2  11953  fprodsplitdc  11992  fprodconst  12016  dvdsle  12240  bitsfzo  12351  dvdsbnd  12362  bezoutlemmain  12404  bezoutlemzz  12408  bezoutlembi  12411  dfgcd3  12416  dvdsmulgcd  12431  nnmindc  12440  lcmcllem  12474  lcmgcdlem  12484  ncoprmgcdne1b  12496  isprm5  12549  pw2dvdslemn  12572  oddpwdclemxy  12576  pythagtriplem2  12674  pythagtrip  12691  pceu  12703  pc2dvds  12738  pcz  12740  pcadd  12748  pcfac  12758  exmidunben  12882  ctiunctlemfo  12895  unct  12898  prdsval  13190  sgrppropd  13330  sgrpidmndm  13337  mndpropd  13357  mhmeql  13409  isgrpinv  13471  dfgrp3mlem  13515  mhmmnd  13537  conjnmzb  13701  ghmcmn  13748  gsumfzconst  13762  isrng  13781  issrg  13812  isring  13847  reldvdsrsrg  13939  dvdsrmul1  13949  tgrest  14726  cnpnei  14776  cnss1  14783  cncnp  14787  ismet2  14911  metequiv2  15053  metcnp  15069  metcnp2  15070  metcnpi3  15074  fsumcncntop  15124  elcncf2  15131  cncfmet  15149  suplociccreex  15181  dedekindicclemicc  15189  ivthinclemlr  15194  ivthinclemur  15196  cnplimclemr  15226  limccnpcntop  15232  limccoap  15235  dvmptfsum  15282  elply2  15292  plyrecj  15320  mersenne  15554  lgsval2lem  15572  lgsquad3  15646  nninfalllem1  16117  nnnninfex  16131  sbthom  16137  apdiff  16159