Theorem negeqd 8416

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

Syntax hints:   → wi 4   = wceq 1398  -cneg 8393

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 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031  df-neg 8395

This theorem is referenced by:  negdi  8478  mulneg2  8617  mulm1  8621  eqord2  8706  mulreim  8826  apneg  8833  divnegap  8928  div2negap  8957  recgt0  9072  infrenegsupex  9872  supminfex  9875  mul2lt0rlt0  10038  ceilqval  10614  ceilid  10623  modqcyc2  10668  monoord2  10794  reneg  11491  imneg  11499  cjcj  11506  cjneg  11513  minmax  11853  minabs  11859  telfsumo2  12091  sinneg  12350  tannegap  12352  sincossq  12372  odd2np1  12497  oexpneg  12501  modgcd  12625  pcneg  12961  mulgval  13772  mulgneg  13790  ivthdec  15438  limcimolemlt  15458  dvrecap  15507  sinperlem  15602  efimpi  15613  ptolemy  15618  lgsneg1  15827  lgseisenlem1  15872  lgseisenlem4  15875  m1lgs  15887  ex-ceil  16423