Theorem supeq1d 7115

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

Hypothesis

Ref	Expression
supeq1d.1	|- ( ph -> B = C )

Assertion

Ref	Expression
supeq1d	|- ( ph -> sup ( B , A , R ) = sup ( C , A , R ) )

Proof of Theorem supeq1d

Step	Hyp	Ref	Expression
1		supeq1d.1	. 2 |- ( ph -> B = C )
2		supeq1 7114	. 2 |- ( B = C -> sup ( B , A , R ) = sup ( C , A , R ) )
3	1, 2	syl 14	1 |- ( ph -> sup ( B , A , R ) = sup ( C , A , R ) )

Syntax hints:   -> wi 4   = wceq 1373   supcsup 7110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-rex 2492  df-rab 2495  df-uni 3865  df-sup 7112

This theorem is referenced by:  sup3exmid  9065  supminfex  9753  suprzubdc  10416  minmax  11656  xrminmax  11691  xrminrecl  11699  xrminadd  11701  gcdval  12395  gcdass  12451  pceulem  12732  pceu  12733  pcval  12734  pczpre  12735  pcdiv  12740  pcneg  12763  prdsex  13216  prdsval  13220  xmetxp  15094  xmetxpbl  15095  txmetcnp  15105  qtopbasss  15108  hovera  15234  hoverb  15235  hoverlt1  15236  hovergt0  15237  ivthdich  15240