Theorem negeqd 8302

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

Syntax hints:   → wi 4   = wceq 1373  -cneg 8279

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-iota 5251  df-fv 5298  df-ov 5970  df-neg 8281

This theorem is referenced by:  negdi  8364  mulneg2  8503  mulm1  8507  eqord2  8592  mulreim  8712  apneg  8719  divnegap  8814  div2negap  8843  recgt0  8958  infrenegsupex  9750  supminfex  9753  mul2lt0rlt0  9916  ceilqval  10488  ceilid  10497  modqcyc2  10542  monoord2  10668  reneg  11294  imneg  11302  cjcj  11309  cjneg  11316  minmax  11656  minabs  11662  telfsumo2  11893  sinneg  12152  tannegap  12154  sincossq  12174  odd2np1  12299  oexpneg  12303  modgcd  12427  pcneg  12763  mulgval  13573  mulgneg  13591  ivthdec  15231  limcimolemlt  15251  dvrecap  15300  sinperlem  15395  efimpi  15406  ptolemy  15411  lgsneg1  15617  lgseisenlem1  15662  lgseisenlem4  15665  m1lgs  15677  ex-ceil  15862