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  6257  tfrlem1  6337  tfr1onlemaccex  6377  tfrcllemaccex  6390  frecabcl  6428  fopwdom  6868  phplem4dom  6894  phpm  6897  phplem4on  6899  fidifsnen  6902  diffisn  6925  diffifi  6926  en2eqpr  6939  fisseneq  6964  suplub2ti  7034  difinfsn  7133  ctmlemr  7141  ctm  7142  ctssdclemn0  7143  ctssdc  7146  nninfninc  7156  nninfisol  7166  enomnilem  7171  enmkvlem  7194  enwomnilem  7202  nninfwlpoimlemginf  7209  exmidontriimlem4  7258  exmidontriim  7259  cc3  7302  addcmpblnq  7401  mulcmpblnq  7402  ordpipqqs  7408  ltexnqq  7442  enq0tr  7468  addcmpblnq0  7477  mulcmpblnq0  7478  nnnq0lem1  7480  prssnqu  7514  prarloclemup  7529  nqprl  7585  nqpru  7586  mullocpr  7605  cauappcvgprlemladdfu  7688  cauappcvgprlemladdrl  7691  caucvgprlemm  7702  caucvgprlemladdfu  7711  caucvgprlemladdrl  7712  caucvgprlemlim  7715  caucvgprprlemml  7728  caucvgprprlemloc  7737  caucvgprprlemlim  7745  suplocexprlemmu  7752  suplocexprlemru  7753  suplocexprlemdisj  7754  suplocexprlemloc  7755  addcmpblnr  7773  mulcmpblnrlemg  7774  mulcmpblnr  7775  ltsrprg  7781  srpospr  7817  caucvgsrlemoffres  7834  suplocsrlemb  7840  suplocsrlempr  7841  suplocsrlem  7842  axcaucvglemcau  7932  axsuploc  8065  cnegexlem3  8169  negeu  8183  add20  8466  rimul  8577  apreap  8579  cru  8594  apreim  8595  apsym  8598  apcotr  8599  apadd1  8600  apneg  8603  mulext1  8604  apti  8614  aptap  8642  mulap0  8646  prodgt0  8844  ltmul12a  8852  ledivdiv  8882  lediv12a  8886  supinfneg  9631  infsupneg  9632  qapne  9675  xaddf  9880  xaddval  9881  xleadd1a  9909  xleaddadd  9923  ixxss12  9942  ioodisj  10029  fznlem  10077  qtri3or  10279  exbtwnzlemstep  10284  rebtwn2zlemstep  10289  addmodlteq  10435  mulexpzap  10600  leexp1a  10615  expnbnd  10684  apexp1  10739  faclbnd  10762  hashxp  10847  zfz1iso  10862  cjap  10956  caucvgre  11031  cvg1nlemres  11035  resqrexlemglsq  11072  resqrexlemga  11073  sqrtsq  11094  ltabs  11137  abs3lem  11161  cau3lem  11164  maxleim  11255  rexico  11271  minmax  11279  xrmaxleim  11293  xrmaxiflemcl  11294  xrmaxiflemlub  11297  xrmaxiflemval  11299  xrmaxltsup  11307  xrmaxadd  11310  xrminmax  11314  xrbdtri  11325  climcau  11396  climrecvg1n  11397  sumeq2  11408  summodclem2  11431  divcnv  11546  prodeq2  11606  fprodsplitdc  11645  fprodconst  11669  dvdsle  11891  zsupcllemstep  11987  dvdsbnd  11998  bezoutlemmain  12040  bezoutlemzz  12044  bezoutlembi  12047  dfgcd3  12052  dvdsmulgcd  12067  nnmindc  12076  lcmcllem  12110  lcmgcdlem  12120  ncoprmgcdne1b  12132  isprm5  12185  pw2dvdslemn  12208  oddpwdclemxy  12212  pythagtriplem2  12309  pythagtrip  12326  pceu  12338  pc2dvds  12373  pcz  12375  pcadd  12383  pcfac  12393  exmidunben  12488  ctiunctlemfo  12501  unct  12504  sgrppropd  12899  sgrpidmndm  12904  mndpropd  12924  mhmeql  12967  isgrpinv  13021  dfgrp3mlem  13065  mhmmnd  13081  conjnmzb  13244  ghmcmn  13290  isrng  13313  issrg  13344  isring  13379  reldvdsrsrg  13467  dvdsrmul1  13477  tgrest  14154  cnpnei  14204  cnss1  14211  cncnp  14215  ismet2  14339  metequiv2  14481  metcnp  14497  metcnp2  14498  metcnpi3  14502  fsumcncntop  14541  elcncf2  14546  cncfmet  14564  suplociccreex  14587  dedekindicclemicc  14595  ivthinclemlr  14600  ivthinclemur  14602  cnplimclemr  14623  limccnpcntop  14629  limccoap  14632  lgsval2lem  14897  nninfalllem1  15244  sbthom  15262  apdiff  15284