Theorem negeqd 8337

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

Hypothesis

Ref	Expression
negeqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
negeqd	⊢ (𝜑 → -𝐴 = -𝐵)

Proof of Theorem negeqd

Step	Hyp	Ref	Expression
1		negeqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		negeq 8335	. 2 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵)
3	1, 2	syl 14	1 ⊢ (𝜑 → -𝐴 = -𝐵)

Syntax hints:   → wi 4   = wceq 1395  -cneg 8314

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 3888  df-br 4083  df-iota 5277  df-fv 5325  df-ov 6003  df-neg 8316

This theorem is referenced by:  negdi  8399  mulneg2  8538  mulm1  8542  eqord2  8627  mulreim  8747  apneg  8754  divnegap  8849  div2negap  8878  recgt0  8993  infrenegsupex  9785  supminfex  9788  mul2lt0rlt0  9951  ceilqval  10523  ceilid  10532  modqcyc2  10577  monoord2  10703  reneg  11374  imneg  11382  cjcj  11389  cjneg  11396  minmax  11736  minabs  11742  telfsumo2  11973  sinneg  12232  tannegap  12234  sincossq  12254  odd2np1  12379  oexpneg  12383  modgcd  12507  pcneg  12843  mulgval  13654  mulgneg  13672  ivthdec  15312  limcimolemlt  15332  dvrecap  15381  sinperlem  15476  efimpi  15487  ptolemy  15492  lgsneg1  15698  lgseisenlem1  15743  lgseisenlem4  15746  m1lgs  15758  ex-ceil  16048