Theorem simpllr 540

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 492	1 |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ps )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  simp-4r  548  f1o2ndf1  6464  tfrlem1  6579  tfr1onlemaccex  6619  tfrcllemaccex  6632  frecabcl  6670  fopwdom  7136  phplem4dom  7163  phpm  7167  phplem4on  7169  fidifsnen  7172  diffisn  7197  diffifi  7198  en2eqpr  7214  fisseneq  7242  suplub2ti  7342  difinfsn  7441  ctmlemr  7449  ctm  7450  ctssdclemn0  7451  ctssdc  7454  nninfninc  7464  nninfisol  7474  enomnilem  7479  enmkvlem  7502  enwomnilem  7510  nninfwlpoimlemginf  7517  exmidontriimlem4  7581  exmidontriim  7582  cc3  7635  addcmpblnq  7735  mulcmpblnq  7736  ordpipqqs  7742  ltexnqq  7776  enq0tr  7802  addcmpblnq0  7811  mulcmpblnq0  7812  nnnq0lem1  7814  prssnqu  7848  prarloclemup  7863  nqprl  7919  nqpru  7920  mullocpr  7939  cauappcvgprlemladdfu  8022  cauappcvgprlemladdrl  8025  caucvgprlemm  8036  caucvgprlemladdfu  8045  caucvgprlemladdrl  8046  caucvgprlemlim  8049  caucvgprprlemml  8062  caucvgprprlemloc  8071  caucvgprprlemlim  8079  suplocexprlemmu  8086  suplocexprlemru  8087  suplocexprlemdisj  8088  suplocexprlemloc  8089  addcmpblnr  8107  mulcmpblnrlemg  8108  mulcmpblnr  8109  ltsrprg  8115  srpospr  8151  caucvgsrlemoffres  8168  suplocsrlemb  8174  suplocsrlempr  8175  suplocsrlem  8176  axcaucvglemcau  8266  axsuploc  8399  cnegexlem3  8505  negeu  8519  add20  8804  rimul  8916  apreap  8918  cru  8933  apreim  8934  apsym  8937  apcotr  8938  apadd1  8939  apneg  8942  mulext1  8943  apti  8953  aptap  8981  mulap0  8985  prodgt0  9185  ltmul12a  9193  ledivdiv  9223  lediv12a  9227  supinfneg  10005  infsupneg  10006  qapne  10049  irraddap  10057  xaddf  10257  xaddval  10258  xleadd1a  10286  xleaddadd  10300  ixxss12  10319  ioodisj  10406  fznlem  10456  zsupcllemstep  10673  qtri3or  10686  exbtwnzlemstep  10693  rebtwn2zlemstep  10698  addmodlteq  10850  seqf1og  10973  mulexpzap  11031  leexp1a  11046  expnbnd  11116  apexp1  11172  faclbnd  11195  hashxp  11283  sshashneg  11297  hashf1lem2  11302  zfz1iso  11309  swrdswrdlem  11492  cjap  11688  caucvgre  11763  cvg1nlemres  11767  resqrexlemglsq  11804  resqrexlemga  11805  sqrtsq  11826  ltabs  11870  abs3lem  11894  cau3lem  11897  maxleim  11988  rexico  12004  fiidxsupcl  12012  minmax  12014  xrmaxleim  12029  xrmaxiflemcl  12030  xrmaxiflemlub  12033  xrmaxiflemval  12035  xrmaxltsup  12043  xrmaxadd  12046  xrminmax  12050  xrbdtri  12061  climcau  12132  climrecvg1n  12133  sumeq2  12144  summodclem2  12168  divcnv  12283  prodeq2  12343  fprodsplitdc  12382  fprodconst  12406  dvdsle  12630  bitsfzo  12741  dvdsbnd  12752  bezoutlemmain  12794  bezoutlemzz  12798  bezoutlembi  12801  dfgcd3  12806  dvdsmulgcd  12821  nnmindc  12830  lcmcllem  12864  lcmgcdlem  12874  ncoprmgcdne1b  12886  isprm5  12940  pwbdvdslemn  12963  nnmaxpwlemparts  12971  pythagtriplem2  13068  pythagtrip  13085  pceu  13097  pc2dvds  13132  pcz  13134  pcadd  13142  pcfac  13152  exmidunben  13369  ctiunctlemfo  13382  unct  13385  sgrppropd  13781  sgrpidmndm  13786  mndpropd  13806  mhmeql  13852  isgrpinv  13912  dfgrp3mlem  13956  mhmmnd  13972  conjnmzb  14136  resscntz  14160  ghmcmn  14215  gzsumconst  14227  prdsval  14257  isrng  14317  issrg  14353  isring  14388  dvdsrmul1  14493  aprlring  14684  issubassa2  15119  tgrest  15361  cnpnei  15411  cnss1  15418  cncnp  15422  ismet2  15546  metequiv2  15688  metcnp  15704  metcnp2  15705  metcnpi3  15709  fsumcncntop  15759  elcncf2  15766  cncfmet  15784  suplociccreex  15816  dedekindicclemicc  15824  ivthinclemlr  15829  ivthinclemur  15831  cnplimclemr  15861  limccnpcntop  15867  limccoap  15870  dvmptfsum  15917  elply2  15927  plyrecj  15955  logdivlt  16088  zprmlogbap  16179  mersenne  16258  lgsval2lem  16295  lgsquad3  16369  usgr1eop  16652  usgr1vr  16655  pw1ndom3  17186  nninfalllem1  17217  nnnninfex  17231  sbthom  17237  apdiff  17264