Theorem simpllr 536

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  544  f1o2ndf1  6402  tfrlem1  6517  tfr1onlemaccex  6557  tfrcllemaccex  6570  frecabcl  6608  fopwdom  7065  phplem4dom  7091  phpm  7095  phplem4on  7097  fidifsnen  7100  diffisn  7125  diffifi  7126  en2eqpr  7142  fisseneq  7170  suplub2ti  7243  difinfsn  7342  ctmlemr  7350  ctm  7351  ctssdclemn0  7352  ctssdc  7355  nninfninc  7365  nninfisol  7375  enomnilem  7380  enmkvlem  7403  enwomnilem  7411  nninfwlpoimlemginf  7418  exmidontriimlem4  7482  exmidontriim  7483  cc3  7530  addcmpblnq  7630  mulcmpblnq  7631  ordpipqqs  7637  ltexnqq  7671  enq0tr  7697  addcmpblnq0  7706  mulcmpblnq0  7707  nnnq0lem1  7709  prssnqu  7743  prarloclemup  7758  nqprl  7814  nqpru  7815  mullocpr  7834  cauappcvgprlemladdfu  7917  cauappcvgprlemladdrl  7920  caucvgprlemm  7931  caucvgprlemladdfu  7940  caucvgprlemladdrl  7941  caucvgprlemlim  7944  caucvgprprlemml  7957  caucvgprprlemloc  7966  caucvgprprlemlim  7974  suplocexprlemmu  7981  suplocexprlemru  7982  suplocexprlemdisj  7983  suplocexprlemloc  7984  addcmpblnr  8002  mulcmpblnrlemg  8003  mulcmpblnr  8004  ltsrprg  8010  srpospr  8046  caucvgsrlemoffres  8063  suplocsrlemb  8069  suplocsrlempr  8070  suplocsrlem  8071  axcaucvglemcau  8161  axsuploc  8294  cnegexlem3  8398  negeu  8412  add20  8696  rimul  8807  apreap  8809  cru  8824  apreim  8825  apsym  8828  apcotr  8829  apadd1  8830  apneg  8833  mulext1  8834  apti  8844  aptap  8872  mulap0  8876  prodgt0  9074  ltmul12a  9082  ledivdiv  9112  lediv12a  9116  supinfneg  9873  infsupneg  9874  qapne  9917  xaddf  10123  xaddval  10124  xleadd1a  10152  xleaddadd  10166  ixxss12  10185  ioodisj  10272  fznlem  10321  zsupcllemstep  10535  qtri3or  10546  exbtwnzlemstep  10553  rebtwn2zlemstep  10558  addmodlteq  10706  seqf1og  10829  mulexpzap  10887  leexp1a  10902  expnbnd  10971  apexp1  11026  faclbnd  11049  hashxp  11136  zfz1iso  11151  swrdswrdlem  11334  cjap  11529  caucvgre  11604  cvg1nlemres  11608  resqrexlemglsq  11645  resqrexlemga  11646  sqrtsq  11667  ltabs  11710  abs3lem  11734  cau3lem  11737  maxleim  11828  rexico  11844  minmax  11853  xrmaxleim  11867  xrmaxiflemcl  11868  xrmaxiflemlub  11871  xrmaxiflemval  11873  xrmaxltsup  11881  xrmaxadd  11884  xrminmax  11888  xrbdtri  11899  climcau  11970  climrecvg1n  11971  sumeq2  11982  summodclem2  12006  divcnv  12121  prodeq2  12181  fprodsplitdc  12220  fprodconst  12244  dvdsle  12468  bitsfzo  12579  dvdsbnd  12590  bezoutlemmain  12632  bezoutlemzz  12636  bezoutlembi  12639  dfgcd3  12644  dvdsmulgcd  12659  nnmindc  12668  lcmcllem  12702  lcmgcdlem  12712  ncoprmgcdne1b  12724  isprm5  12777  pw2dvdslemn  12800  oddpwdclemxy  12804  pythagtriplem2  12902  pythagtrip  12919  pceu  12931  pc2dvds  12966  pcz  12968  pcadd  12976  pcfac  12986  exmidunben  13110  ctiunctlemfo  13123  unct  13126  prdsval  13419  sgrppropd  13559  sgrpidmndm  13566  mndpropd  13586  mhmeql  13638  isgrpinv  13700  dfgrp3mlem  13744  mhmmnd  13766  conjnmzb  13930  ghmcmn  13977  gsumfzconst  13991  isrng  14011  issrg  14042  isring  14077  dvdsrmul1  14180  tgrest  14963  cnpnei  15013  cnss1  15020  cncnp  15024  ismet2  15148  metequiv2  15290  metcnp  15306  metcnp2  15307  metcnpi3  15311  fsumcncntop  15361  elcncf2  15368  cncfmet  15386  suplociccreex  15418  dedekindicclemicc  15426  ivthinclemlr  15431  ivthinclemur  15433  cnplimclemr  15463  limccnpcntop  15469  limccoap  15472  dvmptfsum  15519  elply2  15529  plyrecj  15557  mersenne  15794  lgsval2lem  15812  lgsquad3  15886  usgr1eop  16169  usgr1vr  16172  pw1ndom3  16693  nninfalllem1  16717  nnnninfex  16731  sbthom  16737  apdiff  16763