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  6380  tfrlem1  6460  tfr1onlemaccex  6500  tfrcllemaccex  6513  frecabcl  6551  fopwdom  7005  phplem4dom  7031  phpm  7035  phplem4on  7037  fidifsnen  7040  diffisn  7063  diffifi  7064  en2eqpr  7080  fisseneq  7107  suplub2ti  7179  difinfsn  7278  ctmlemr  7286  ctm  7287  ctssdclemn0  7288  ctssdc  7291  nninfninc  7301  nninfisol  7311  enomnilem  7316  enmkvlem  7339  enwomnilem  7347  nninfwlpoimlemginf  7354  exmidontriimlem4  7417  exmidontriim  7418  cc3  7465  addcmpblnq  7565  mulcmpblnq  7566  ordpipqqs  7572  ltexnqq  7606  enq0tr  7632  addcmpblnq0  7641  mulcmpblnq0  7642  nnnq0lem1  7644  prssnqu  7678  prarloclemup  7693  nqprl  7749  nqpru  7750  mullocpr  7769  cauappcvgprlemladdfu  7852  cauappcvgprlemladdrl  7855  caucvgprlemm  7866  caucvgprlemladdfu  7875  caucvgprlemladdrl  7876  caucvgprlemlim  7879  caucvgprprlemml  7892  caucvgprprlemloc  7901  caucvgprprlemlim  7909  suplocexprlemmu  7916  suplocexprlemru  7917  suplocexprlemdisj  7918  suplocexprlemloc  7919  addcmpblnr  7937  mulcmpblnrlemg  7938  mulcmpblnr  7939  ltsrprg  7945  srpospr  7981  caucvgsrlemoffres  7998  suplocsrlemb  8004  suplocsrlempr  8005  suplocsrlem  8006  axcaucvglemcau  8096  axsuploc  8230  cnegexlem3  8334  negeu  8348  add20  8632  rimul  8743  apreap  8745  cru  8760  apreim  8761  apsym  8764  apcotr  8765  apadd1  8766  apneg  8769  mulext1  8770  apti  8780  aptap  8808  mulap0  8812  prodgt0  9010  ltmul12a  9018  ledivdiv  9048  lediv12a  9052  supinfneg  9802  infsupneg  9803  qapne  9846  xaddf  10052  xaddval  10053  xleadd1a  10081  xleaddadd  10095  ixxss12  10114  ioodisj  10201  fznlem  10249  zsupcllemstep  10461  qtri3or  10472  exbtwnzlemstep  10479  rebtwn2zlemstep  10484  addmodlteq  10632  seqf1og  10755  mulexpzap  10813  leexp1a  10828  expnbnd  10897  apexp1  10952  faclbnd  10975  hashxp  11061  zfz1iso  11076  swrdswrdlem  11251  cjap  11432  caucvgre  11507  cvg1nlemres  11511  resqrexlemglsq  11548  resqrexlemga  11549  sqrtsq  11570  ltabs  11613  abs3lem  11637  cau3lem  11640  maxleim  11731  rexico  11747  minmax  11756  xrmaxleim  11770  xrmaxiflemcl  11771  xrmaxiflemlub  11774  xrmaxiflemval  11776  xrmaxltsup  11784  xrmaxadd  11787  xrminmax  11791  xrbdtri  11802  climcau  11873  climrecvg1n  11874  sumeq2  11885  summodclem2  11908  divcnv  12023  prodeq2  12083  fprodsplitdc  12122  fprodconst  12146  dvdsle  12370  bitsfzo  12481  dvdsbnd  12492  bezoutlemmain  12534  bezoutlemzz  12538  bezoutlembi  12541  dfgcd3  12546  dvdsmulgcd  12561  nnmindc  12570  lcmcllem  12604  lcmgcdlem  12614  ncoprmgcdne1b  12626  isprm5  12679  pw2dvdslemn  12702  oddpwdclemxy  12706  pythagtriplem2  12804  pythagtrip  12821  pceu  12833  pc2dvds  12868  pcz  12870  pcadd  12878  pcfac  12888  exmidunben  13012  ctiunctlemfo  13025  unct  13028  prdsval  13321  sgrppropd  13461  sgrpidmndm  13468  mndpropd  13488  mhmeql  13540  isgrpinv  13602  dfgrp3mlem  13646  mhmmnd  13668  conjnmzb  13832  ghmcmn  13879  gsumfzconst  13893  isrng  13912  issrg  13943  isring  13978  dvdsrmul1  14081  tgrest  14858  cnpnei  14908  cnss1  14915  cncnp  14919  ismet2  15043  metequiv2  15185  metcnp  15201  metcnp2  15202  metcnpi3  15206  fsumcncntop  15256  elcncf2  15263  cncfmet  15281  suplociccreex  15313  dedekindicclemicc  15321  ivthinclemlr  15326  ivthinclemur  15328  cnplimclemr  15358  limccnpcntop  15364  limccoap  15367  dvmptfsum  15414  elply2  15424  plyrecj  15452  mersenne  15686  lgsval2lem  15704  lgsquad3  15778  pw1ndom3  16413  nninfalllem1  16434  nnnninfex  16448  sbthom  16454  apdiff  16476