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  6372  tfrlem1  6452  tfr1onlemaccex  6492  tfrcllemaccex  6505  frecabcl  6543  fopwdom  6993  phplem4dom  7019  phpm  7023  phplem4on  7025  fidifsnen  7028  diffisn  7051  diffifi  7052  en2eqpr  7065  fisseneq  7092  suplub2ti  7164  difinfsn  7263  ctmlemr  7271  ctm  7272  ctssdclemn0  7273  ctssdc  7276  nninfninc  7286  nninfisol  7296  enomnilem  7301  enmkvlem  7324  enwomnilem  7332  nninfwlpoimlemginf  7339  exmidontriimlem4  7402  exmidontriim  7403  cc3  7450  addcmpblnq  7550  mulcmpblnq  7551  ordpipqqs  7557  ltexnqq  7591  enq0tr  7617  addcmpblnq0  7626  mulcmpblnq0  7627  nnnq0lem1  7629  prssnqu  7663  prarloclemup  7678  nqprl  7734  nqpru  7735  mullocpr  7754  cauappcvgprlemladdfu  7837  cauappcvgprlemladdrl  7840  caucvgprlemm  7851  caucvgprlemladdfu  7860  caucvgprlemladdrl  7861  caucvgprlemlim  7864  caucvgprprlemml  7877  caucvgprprlemloc  7886  caucvgprprlemlim  7894  suplocexprlemmu  7901  suplocexprlemru  7902  suplocexprlemdisj  7903  suplocexprlemloc  7904  addcmpblnr  7922  mulcmpblnrlemg  7923  mulcmpblnr  7924  ltsrprg  7930  srpospr  7966  caucvgsrlemoffres  7983  suplocsrlemb  7989  suplocsrlempr  7990  suplocsrlem  7991  axcaucvglemcau  8081  axsuploc  8215  cnegexlem3  8319  negeu  8333  add20  8617  rimul  8728  apreap  8730  cru  8745  apreim  8746  apsym  8749  apcotr  8750  apadd1  8751  apneg  8754  mulext1  8755  apti  8765  aptap  8793  mulap0  8797  prodgt0  8995  ltmul12a  9003  ledivdiv  9033  lediv12a  9037  supinfneg  9786  infsupneg  9787  qapne  9830  xaddf  10036  xaddval  10037  xleadd1a  10065  xleaddadd  10079  ixxss12  10098  ioodisj  10185  fznlem  10233  zsupcllemstep  10444  qtri3or  10455  exbtwnzlemstep  10462  rebtwn2zlemstep  10467  addmodlteq  10615  seqf1og  10738  mulexpzap  10796  leexp1a  10811  expnbnd  10880  apexp1  10935  faclbnd  10958  hashxp  11043  zfz1iso  11058  swrdswrdlem  11231  cjap  11412  caucvgre  11487  cvg1nlemres  11491  resqrexlemglsq  11528  resqrexlemga  11529  sqrtsq  11550  ltabs  11593  abs3lem  11617  cau3lem  11620  maxleim  11711  rexico  11727  minmax  11736  xrmaxleim  11750  xrmaxiflemcl  11751  xrmaxiflemlub  11754  xrmaxiflemval  11756  xrmaxltsup  11764  xrmaxadd  11767  xrminmax  11771  xrbdtri  11782  climcau  11853  climrecvg1n  11854  sumeq2  11865  summodclem2  11888  divcnv  12003  prodeq2  12063  fprodsplitdc  12102  fprodconst  12126  dvdsle  12350  bitsfzo  12461  dvdsbnd  12472  bezoutlemmain  12514  bezoutlemzz  12518  bezoutlembi  12521  dfgcd3  12526  dvdsmulgcd  12541  nnmindc  12550  lcmcllem  12584  lcmgcdlem  12594  ncoprmgcdne1b  12606  isprm5  12659  pw2dvdslemn  12682  oddpwdclemxy  12686  pythagtriplem2  12784  pythagtrip  12801  pceu  12813  pc2dvds  12848  pcz  12850  pcadd  12858  pcfac  12868  exmidunben  12992  ctiunctlemfo  13005  unct  13008  prdsval  13301  sgrppropd  13441  sgrpidmndm  13448  mndpropd  13468  mhmeql  13520  isgrpinv  13582  dfgrp3mlem  13626  mhmmnd  13648  conjnmzb  13812  ghmcmn  13859  gsumfzconst  13873  isrng  13892  issrg  13923  isring  13958  reldvdsrsrg  14050  dvdsrmul1  14060  tgrest  14837  cnpnei  14887  cnss1  14894  cncnp  14898  ismet2  15022  metequiv2  15164  metcnp  15180  metcnp2  15181  metcnpi3  15185  fsumcncntop  15235  elcncf2  15242  cncfmet  15260  suplociccreex  15292  dedekindicclemicc  15300  ivthinclemlr  15305  ivthinclemur  15307  cnplimclemr  15337  limccnpcntop  15343  limccoap  15346  dvmptfsum  15393  elply2  15403  plyrecj  15431  mersenne  15665  lgsval2lem  15683  lgsquad3  15757  nninfalllem1  16333  nnnninfex  16347  sbthom  16353  apdiff  16375