Theorem negeqd 8468

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

Syntax hints:   -> wi 4   = wceq 1398   -ucneg 8445

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-iota 5312  df-fv 5360  df-ov 6053  df-neg 8447

This theorem is referenced by:  negdi  8530  mulneg2  8669  mulm1  8673  eqord2  8758  mulreim  8878  apneg  8885  divnegap  8980  div2negap  9009  recgt0  9124  infrenegsupex  9926  supminfex  9929  mul2lt0rlt0  10092  ceilqval  10668  ceilid  10677  modqcyc2  10722  monoord2  10848  reneg  11553  imneg  11561  cjcj  11568  cjneg  11575  minmax  11915  minabs  11921  telfsumo2  12153  sinneg  12412  tannegap  12414  sincossq  12434  odd2np1  12559  oexpneg  12563  modgcd  12687  pcneg  13023  mulgval  13839  mulgneg  13857  ivthdec  15509  limcimolemlt  15529  dvrecap  15578  sinperlem  15673  efimpi  15684  ptolemy  15689  lgsneg1  15898  lgseisenlem1  15943  lgseisenlem4  15946  m1lgs  15958  ex-ceil  16494