Theorem supeq1d 8235

Description: Equality deduction for supremum. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
supeq1d.1	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
supeq1d	⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))

Proof of Theorem supeq1d

Step	Hyp	Ref	Expression
1		supeq1d.1	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
2		supeq1 8234	. 2 ⊢ (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
3	1, 2	syl 17	1 ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))

Syntax hints:   → wi 4   = wceq 1475  supcsup 8229

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-uni 4373  df-sup 8231

This theorem is referenced by:  supadd  10868  supminf  11651  rpnnen1lem6  11695  rpnnen1  11696  rpnnen1OLD  11701  limsupval  14053  limsupgval  14055  gcdval  15056  gcdass  15102  pcval  15387  pceulem  15388  pceu  15389  pczpre  15390  pcdiv  15395  pcneg  15416  prmreclem1  15458  prmreclem5  15462  ramz  15567  prdsval  15938  prdsdsval  15961  prdsdsval2  15967  prdsdsval3  15968  ressprdsds  21986  xpsdsval  21996  tmsxpsval  22153  bndth  22565  elovolmr  23051  ovolctb  23065  ovoliunlem3  23079  ovolshftlem1  23084  voliunlem3  23127  voliun  23129  volsup  23131  ioorf  23147  mbfinf  23238  itg1climres  23287  itg2val  23301  itg2monolem1  23323  itg2i1fseq  23328  itg2cnlem1  23334  mdegfval  23626  mdegval  23627  mdeg0  23634  mdegvsca  23640  mdegpropd  23648  deg1val  23660  deg1mul3  23679  dgrval  23788  coe11  23813  nmoofval  27001  nmooval  27002  nmoo0  27030  nmopval  28099  nmfnval  28119  esumval  29435  esum0  29438  esumsnf  29453  esumfsupre  29460  esumsup  29478  erdszelem3  30429  erdsze  30438  elwlim  31013  elwlimOLD  31014  ee7.2aOLD  31630  poimirlem32  32611  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  itg2addnc  32634  aomclem8  36649  supsubc  38510  fourierdlem79  39078  fourierdlem96  39095  fourierdlem97  39096  fourierdlem98  39097  fourierdlem99  39098  fourierdlem105  39104  fourierdlem108  39107  fourierdlem110  39109  sge0val  39259  sge0z  39268  sge0revalmpt  39271  sge0sn  39272  sge0tsms  39273  sge0f1o  39275  sge0sup  39284  sge0resplit  39299  meaiuninclem  39373