Theorem negeqd 8341

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 8339	. 2 |- ( A = B -> -u A = -u B )
3	1, 2	syl 14	1 |- ( ph -> -u A = -u B )

Syntax hints:   -> wi 4   = wceq 1395   -ucneg 8318

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6004  df-neg 8320

This theorem is referenced by:  negdi  8403  mulneg2  8542  mulm1  8546  eqord2  8631  mulreim  8751  apneg  8758  divnegap  8853  div2negap  8882  recgt0  8997  infrenegsupex  9789  supminfex  9792  mul2lt0rlt0  9955  ceilqval  10528  ceilid  10537  modqcyc2  10582  monoord2  10708  reneg  11379  imneg  11387  cjcj  11394  cjneg  11401  minmax  11741  minabs  11747  telfsumo2  11978  sinneg  12237  tannegap  12239  sincossq  12259  odd2np1  12384  oexpneg  12388  modgcd  12512  pcneg  12848  mulgval  13659  mulgneg  13677  ivthdec  15318  limcimolemlt  15338  dvrecap  15387  sinperlem  15482  efimpi  15493  ptolemy  15498  lgsneg1  15704  lgseisenlem1  15749  lgseisenlem4  15752  m1lgs  15764  ex-ceil  16090