Theorem simpllr 529

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 109	. 2 |- ( ( ph /\ ps ) -> ps )
2	1	ad2antrr 485	1 |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  simp-4r  537  f1o2ndf1  6204  tfrlem1  6284  tfr1onlemaccex  6324  tfrcllemaccex  6337  frecabcl  6375  fopwdom  6810  phplem4dom  6836  phpm  6839  phplem4on  6841  fidifsnen  6844  diffisn  6867  diffifi  6868  en2eqpr  6881  fisseneq  6905  suplub2ti  6974  difinfsn  7073  ctmlemr  7081  ctm  7082  ctssdclemn0  7083  ctssdc  7086  nninfisol  7105  enomnilem  7110  enmkvlem  7133  enwomnilem  7141  exmidontriimlem4  7188  exmidontriim  7189  cc3  7217  addcmpblnq  7316  mulcmpblnq  7317  ordpipqqs  7323  ltexnqq  7357  enq0tr  7383  addcmpblnq0  7392  mulcmpblnq0  7393  nnnq0lem1  7395  prssnqu  7429  prarloclemup  7444  nqprl  7500  nqpru  7501  mullocpr  7520  cauappcvgprlemladdfu  7603  cauappcvgprlemladdrl  7606  caucvgprlemm  7617  caucvgprlemladdfu  7626  caucvgprlemladdrl  7627  caucvgprlemlim  7630  caucvgprprlemml  7643  caucvgprprlemloc  7652  caucvgprprlemlim  7660  suplocexprlemmu  7667  suplocexprlemru  7668  suplocexprlemdisj  7669  suplocexprlemloc  7670  addcmpblnr  7688  mulcmpblnrlemg  7689  mulcmpblnr  7690  ltsrprg  7696  srpospr  7732  caucvgsrlemoffres  7749  suplocsrlemb  7755  suplocsrlempr  7756  suplocsrlem  7757  axcaucvglemcau  7847  axsuploc  7979  cnegexlem3  8083  negeu  8097  add20  8380  rimul  8491  apreap  8493  cru  8508  apreim  8509  apsym  8512  apcotr  8513  apadd1  8514  apneg  8517  mulext1  8518  apti  8528  mulap0  8559  prodgt0  8755  ltmul12a  8763  ledivdiv  8793  lediv12a  8797  supinfneg  9541  infsupneg  9542  qapne  9585  xaddf  9788  xaddval  9789  xleadd1a  9817  xleaddadd  9831  ixxss12  9850  ioodisj  9937  fznlem  9984  qtri3or  10186  exbtwnzlemstep  10191  rebtwn2zlemstep  10196  addmodlteq  10341  mulexpzap  10503  leexp1a  10518  expnbnd  10586  apexp1  10639  faclbnd  10662  hashxp  10748  zfz1iso  10763  cjap  10857  caucvgre  10932  cvg1nlemres  10936  resqrexlemglsq  10973  resqrexlemga  10974  sqrtsq  10995  ltabs  11038  abs3lem  11062  cau3lem  11065  maxleim  11156  rexico  11172  minmax  11180  xrmaxleim  11194  xrmaxiflemcl  11195  xrmaxiflemlub  11198  xrmaxiflemval  11200  xrmaxltsup  11208  xrmaxadd  11211  xrminmax  11215  xrbdtri  11226  climcau  11297  climrecvg1n  11298  sumeq2  11309  summodclem2  11332  divcnv  11447  prodeq2  11507  fprodsplitdc  11546  fprodconst  11570  dvdsle  11791  zsupcllemstep  11887  dvdsbnd  11898  gcdsupex  11899  gcdsupcl  11900  bezoutlemmain  11940  bezoutlemzz  11944  bezoutlembi  11947  dfgcd3  11952  dvdsmulgcd  11967  nnmindc  11976  lcmcllem  12008  lcmgcdlem  12018  ncoprmgcdne1b  12030  isprm5  12083  pw2dvdslemn  12106  oddpwdclemxy  12110  pythagtriplem2  12207  pythagtrip  12224  pceu  12236  pc2dvds  12270  pcz  12272  pcadd  12280  pcfac  12289  exmidunben  12368  ctiunctlemfo  12381  unct  12384  sgrpidmndm  12642  mndpropd  12662  mhmeql  12693  tgrest  12884  cnpnei  12934  cnss1  12941  cncnp  12945  ismet2  13069  metequiv2  13211  metcnp  13227  metcnp2  13228  metcnpi3  13232  fsumcncntop  13271  elcncf2  13276  cncfmet  13294  suplociccreex  13317  dedekindicclemicc  13325  ivthinclemlr  13330  ivthinclemur  13332  cnplimclemr  13353  limccnpcntop  13359  limccoap  13362  lgsval2lem  13626  nninfalllem1  13963  sbthom  13980  apdiff  14002