Theorem negeqi 11375

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

Syntax hints:   = wceq 1541  -cneg 11367

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-neg 11369

This theorem is referenced by:  negsubdii  11468  recgt0ii  12050  m1expcl2  14010  crreczi  14153  absi  15211  geo2sum2  15799  bpoly2  15982  bpoly3  15983  sinhval  16081  coshval  16082  cos2bnd  16115  divalglem2  16324  m1expaddsub  19429  cnmsgnsubg  21534  psgninv  21539  ncvspi  25114  cphipval2  25199  ditg0  25812  cbvditg  25813  ang180lem2  26778  ang180lem3  26779  ang180lem4  26780  1cubrlem  26809  dcubic2  26812  atandm2  26845  efiasin  26856  asinsinlem  26859  asinsin  26860  asin1  26862  reasinsin  26864  atancj  26878  atantayl2  26906  ppiub  27173  lgseisenlem1  27344  lgseisenlem2  27345  lgsquadlem1  27349  ostth3  27607  nvpi  30744  ipidsq  30787  ipasslem10  30916  normlem1  31187  polid2i  31234  lnophmlem2  32094  archirngz  33273  cos9thpiminplylem1  33941  cos9thpiminplylem5  33945  xrge0iif1  34097  ballotlem2  34648  ditgeq123i  36405  cbvditgvw2  36445  itg2addnclem3  37876  dvasin  37907  areacirc  37916  cos2t3rdpi  42630  sin4t3rdpi  42631  cos4t3rdpi  42632  lhe4.4ex1a  44591  itgsin0pilem1  46215  stoweidlem26  46291  dirkertrigeqlem3  46365  fourierdlem103  46474  sqwvfourb  46494  fourierswlem  46495  proththd  47881