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 1540  -cneg 11467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-ov 7408  df-neg 11469

This theorem is referenced by:  negsubdii  11568  recgt0ii  12148  m1expcl2  14103  crreczi  14246  absi  15305  geo2sum2  15890  bpoly2  16073  bpoly3  16074  sinhval  16172  coshval  16173  cos2bnd  16206  divalglem2  16414  m1expaddsub  19479  cnmsgnsubg  21537  psgninv  21542  ncvspi  25108  cphipval2  25193  ditg0  25806  cbvditg  25807  ang180lem2  26772  ang180lem3  26773  ang180lem4  26774  1cubrlem  26803  dcubic2  26806  atandm2  26839  efiasin  26850  asinsinlem  26853  asinsin  26854  asin1  26856  reasinsin  26858  atancj  26872  atantayl2  26900  ppiub  27167  lgseisenlem1  27338  lgseisenlem2  27339  lgsquadlem1  27343  ostth3  27601  nvpi  30648  ipidsq  30691  ipasslem10  30820  normlem1  31091  polid2i  31138  lnophmlem2  31998  archirngz  33187  cos9thpiminplylem1  33816  cos9thpiminplylem5  33820  xrge0iif1  33969  ballotlem2  34521  ditgeq123i  36227  cbvditgvw2  36267  itg2addnclem3  37697  dvasin  37728  areacirc  37737  lhe4.4ex1a  44353  itgsin0pilem1  45979  stoweidlem26  46055  dirkertrigeqlem3  46129  fourierdlem103  46238  sqwvfourb  46258  fourierswlem  46259  proththd  47628