Theorem negeqi 11475

Description: Equality inference for negatives. (Contributed by NM, 14-Feb-1995.)

Hypothesis

Ref	Expression
negeqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
negeqi	⊢ -𝐴 = -𝐵

Proof of Theorem negeqi

Step	Hyp	Ref	Expression
1		negeqi.1	. 2 ⊢ 𝐴 = 𝐵
2		negeq 11474	. 2 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵)
3	1, 2	ax-mp 5	1 ⊢ -𝐴 = -𝐵

Syntax hints:   = wceq 1534  -cneg 11467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-iota 6494  df-fv 6550  df-ov 7417  df-neg 11469

This theorem is referenced by:  negsubdii  11567  recgt0ii  12142  m1expcl2  14074  crreczi  14214  absi  15257  geo2sum2  15844  bpoly2  16025  bpoly3  16026  sinhval  16122  coshval  16123  cos2bnd  16156  divalglem2  16363  m1expaddsub  19444  cnmsgnsubg  21496  psgninv  21501  ncvspi  25071  cphipval2  25156  ditg0  25769  cbvditg  25770  ang180lem2  26729  ang180lem3  26730  ang180lem4  26731  1cubrlem  26760  dcubic2  26763  atandm2  26796  efiasin  26807  asinsinlem  26810  asinsin  26811  asin1  26813  reasinsin  26815  atancj  26829  atantayl2  26857  ppiub  27124  lgseisenlem1  27295  lgseisenlem2  27296  lgsquadlem1  27300  ostth3  27558  nvpi  30464  ipidsq  30507  ipasslem10  30636  normlem1  30907  polid2i  30954  lnophmlem2  31814  archirngz  32875  xrge0iif1  33475  ballotlem2  34044  itg2addnclem3  37081  dvasin  37112  areacirc  37121  lhe4.4ex1a  43689  itgsin0pilem1  45261  stoweidlem26  45337  dirkertrigeqlem3  45411  fourierdlem103  45520  sqwvfourb  45540  fourierswlem  45541  proththd  46877