Theorem negeqi 11371

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 11370	. 2 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵)
3	1, 2	ax-mp 5	1 ⊢ -𝐴 = -𝐵

Syntax hints:   = wceq 1541  -cneg 11363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359  df-neg 11365

This theorem is referenced by:  negsubdii  11464  recgt0ii  12046  m1expcl2  14006  crreczi  14149  absi  15207  geo2sum2  15795  bpoly2  15978  bpoly3  15979  sinhval  16077  coshval  16078  cos2bnd  16111  divalglem2  16320  m1expaddsub  19425  cnmsgnsubg  21530  psgninv  21535  ncvspi  25110  cphipval2  25195  ditg0  25808  cbvditg  25809  ang180lem2  26774  ang180lem3  26775  ang180lem4  26776  1cubrlem  26805  dcubic2  26808  atandm2  26841  efiasin  26852  asinsinlem  26855  asinsin  26856  asin1  26858  reasinsin  26860  atancj  26874  atantayl2  26902  ppiub  27169  lgseisenlem1  27340  lgseisenlem2  27341  lgsquadlem1  27345  ostth3  27603  nvpi  30691  ipidsq  30734  ipasslem10  30863  normlem1  31134  polid2i  31181  lnophmlem2  32041  archirngz  33220  cos9thpiminplylem1  33888  cos9thpiminplylem5  33892  xrge0iif1  34044  ballotlem2  34595  ditgeq123i  36352  cbvditgvw2  36392  itg2addnclem3  37813  dvasin  37844  areacirc  37853  cos2t3rdpi  42551  sin4t3rdpi  42552  cos4t3rdpi  42553  lhe4.4ex1a  44512  itgsin0pilem1  46136  stoweidlem26  46212  dirkertrigeqlem3  46286  fourierdlem103  46395  sqwvfourb  46415  fourierswlem  46416  proththd  47802