Theorem negeqi 11445

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

Syntax hints:   = wceq 1570  -cneg 11437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-neg 11439

This theorem is referenced by:  negsubdii  11538  recgt0ii  12116  m1expcl2  14117  crreczi  14260  absi  15333  geo2sum2  15924  bpoly2  16106  bpoly3  16107  sinhval  16205  coshval  16206  cos2bnd  16239  divalglem2  16448  m1expaddsub  19563  cnmsgnsubg  21727  psgninv  21732  ncvspi  25315  cphipval2  25400  ditg0  26012  cbvditg  26013  ang180lem2  26975  ang180lem3  26976  ang180lem4  26977  1cubrlem  27006  dcubic2  27009  atandm2  27042  efiasin  27053  asinsinlem  27056  asinsin  27057  asin1  27059  reasinsin  27061  atancj  27075  atantayl2  27103  ppiub  27368  lgseisenlem1  27539  lgseisenlem2  27540  lgsquadlem1  27544  ostth3  27802  nvpi  31019  ipidsq  31062  ipasslem10  31191  normlem1  31462  polid2i  31509  lnophmlem2  32369  archirngz  33509  cos9thpiminplylem1  34172  cos9thpiminplylem5  34176  xrge0iif1  34328  ballotlem2  34879  ditgeq123i  36741  cbvditgvw2  36781  itg2addnclem3  38344  dvasin  38375  areacirc  38384  25or6to4  42993  cos2t3rdpi  43135  sin4t3rdpi  43136  cos4t3rdpi  43137  lhe4.4ex1a  45059  itgsin0pilem1  46684  stoweidlem26  46760  dirkertrigeqlem3  46834  fourierdlem103  46943  sqwvfourb  46963  fourierswlem  46964  proththd  48386