Theorem negeqd 8364

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 8362	. 2 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵)
3	1, 2	syl 14	1 ⊢ (𝜑 → -𝐴 = -𝐵)

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

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 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332  df-ov 6016  df-neg 8343

This theorem is referenced by:  negdi  8426  mulneg2  8565  mulm1  8569  eqord2  8654  mulreim  8774  apneg  8781  divnegap  8876  div2negap  8905  recgt0  9020  infrenegsupex  9818  supminfex  9821  mul2lt0rlt0  9984  ceilqval  10558  ceilid  10567  modqcyc2  10612  monoord2  10738  reneg  11419  imneg  11427  cjcj  11434  cjneg  11441  minmax  11781  minabs  11787  telfsumo2  12018  sinneg  12277  tannegap  12279  sincossq  12299  odd2np1  12424  oexpneg  12428  modgcd  12552  pcneg  12888  mulgval  13699  mulgneg  13717  ivthdec  15358  limcimolemlt  15378  dvrecap  15427  sinperlem  15522  efimpi  15533  ptolemy  15538  lgsneg1  15744  lgseisenlem1  15789  lgseisenlem4  15792  m1lgs  15804  ex-ceil  16258