Theorem negeqd 8154

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

Syntax hints:   → wi 4   = wceq 1353  -cneg 8131

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2741  df-un 3135  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-iota 5180  df-fv 5226  df-ov 5880  df-neg 8133

This theorem is referenced by:  negdi  8216  mulneg2  8355  mulm1  8359  eqord2  8443  mulreim  8563  apneg  8570  divnegap  8665  div2negap  8694  recgt0  8809  infrenegsupex  9596  supminfex  9599  mul2lt0rlt0  9761  ceilqval  10308  ceilid  10317  modqcyc2  10362  monoord2  10479  reneg  10879  imneg  10887  cjcj  10894  cjneg  10901  minmax  11240  minabs  11246  telfsumo2  11477  sinneg  11736  tannegap  11738  sincossq  11758  odd2np1  11880  oexpneg  11884  modgcd  11994  pcneg  12326  mulgval  12991  mulgneg  13006  ivthdec  14161  limcimolemlt  14172  dvrecap  14216  sinperlem  14268  efimpi  14279  ptolemy  14284  lgsneg1  14465  lgseisenlem1  14489  m1lgs  14491  ex-ceil  14517