Theorem negeqd 8118

Description: Equality deduction for negatives. (Contributed by NM, 14-May-1999.)

Hypothesis

Ref	Expression
negeqd.1	|- ( ph -> A = B )

Assertion

Ref	Expression
negeqd	|- ( ph -> -u A = -u B )

Proof of Theorem negeqd

Step	Hyp	Ref	Expression
1		negeqd.1	. 2 |- ( ph -> A = B )
2		negeq 8116	. 2 |- ( A = B -> -u A = -u B )
3	1, 2	syl 14	1 |- ( ph -> -u A = -u B )

Syntax hints:   -> wi 4   = wceq 1349   -ucneg 8095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-ext 2153

This theorem depends on definitions:  df-bi 116  df-3an 976  df-tru 1352  df-nf 1455  df-sb 1757  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-rex 2455  df-v 2733  df-un 3126  df-sn 3590  df-pr 3591  df-op 3593  df-uni 3798  df-br 3991  df-iota 5162  df-fv 5208  df-ov 5860  df-neg 8097

This theorem is referenced by:  negdi  8180  mulneg2  8319  mulm1  8323  eqord2  8407  mulreim  8527  apneg  8534  divnegap  8627  div2negap  8656  recgt0  8770  infrenegsupex  9557  supminfex  9560  mul2lt0rlt0  9720  ceilqval  10266  ceilid  10275  modqcyc2  10320  monoord2  10437  reneg  10836  imneg  10844  cjcj  10851  cjneg  10858  minmax  11197  minabs  11203  telfsumo2  11434  sinneg  11693  tannegap  11695  sincossq  11715  odd2np1  11836  oexpneg  11840  modgcd  11950  pcneg  12282  mulgval  12819  mulgneg  12834  ivthdec  13501  limcimolemlt  13512  dvrecap  13556  sinperlem  13608  efimpi  13619  ptolemy  13624  lgsneg1  13805  ex-ceil  13846