Theorem neeq2 3050

Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.)

Assertion

Ref	Expression
neeq2	⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))

Proof of Theorem neeq2

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	neeq2d 3047	1 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ≠ wne 2987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-ne 2988

This theorem is referenced by:  psseq2  4016  prproe  4798  fprg  6894  f1dom3el3dif  7005  f1prex  7018  dfac5  9539  kmlem4  9564  kmlem14  9574  1re  10630  hashge2el2difr  13835  hashdmpropge2  13837  dvdsle  15652  sgrp2rid2ex  18084  isirred  19445  isnzr2  20029  dmatelnd  21101  mdetdiaglem  21203  mdetunilem1  21217  mdetunilem2  21218  maducoeval2  21245  hausnei  21933  regr1lem2  22345  xrhmeo  23551  axtg5seg  26259  axtgupdim2  26265  axtgeucl  26266  ishlg  26396  tglnpt2  26435  axlowdim1  26753  umgrvad2edg  27003  2pthdlem1  27716  3pthdlem1  27949  upgr3v3e3cycl  27965  upgr4cycl4dv4e  27970  eupth2lem3lem4  28016  3cyclfrgrrn1  28070  4cycl2vnunb  28075  numclwwlkovh  28158  numclwwlkovq  28159  numclwwlk2lem1  28161  numclwlk2lem2f  28162  superpos  30137  signswch  31941  axtgupdim2ALTV  32049  dfrdg4  33525  fvray  33715  linedegen  33717  fvline  33718  linethru  33727  hilbert1.1  33728  knoppndvlem21  33984  poimirlem1  35058  hlsuprexch  36677  3dim1lem5  36762  llni2  36808  lplni2  36833  2llnjN  36863  lvoli2  36877  2lplnj  36916  islinei  37036  cdleme40n  37764  cdlemg33b  38003  ax6e2ndeq  41265  ax6e2ndeqVD  41615  ax6e2ndeqALT  41637  refsum2cnlem1  41666  stoweidlem43  42685  nnfoctbdjlem  43094  elprneb  43621  ichnreuop  43989  inlinecirc02plem  45200