Theorem neeq2 3081

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 3078	1 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   ≠ wne 3018

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 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-ne 3019

This theorem is referenced by:  psseq2  4067  prproe  4838  fprg  6919  f1dom3el3dif  7029  f1prex  7042  dfac5  9556  kmlem4  9581  kmlem14  9591  1re  10643  hashge2el2difr  13842  hashdmpropge2  13844  dvdsle  15662  sgrp2rid2ex  18094  isirred  19451  isnzr2  20038  dmatelnd  21107  mdetdiaglem  21209  mdetunilem1  21223  mdetunilem2  21224  maducoeval2  21251  hausnei  21938  regr1lem2  22350  xrhmeo  23552  axtg5seg  26253  axtgupdim2  26259  axtgeucl  26260  ishlg  26390  tglnpt2  26429  axlowdim1  26747  umgrvad2edg  26997  2pthdlem1  27711  3pthdlem1  27945  upgr3v3e3cycl  27961  upgr4cycl4dv4e  27966  eupth2lem3lem4  28012  3cyclfrgrrn1  28066  4cycl2vnunb  28071  numclwwlkovh  28154  numclwwlkovq  28155  numclwwlk2lem1  28157  numclwlk2lem2f  28158  superpos  30133  signswch  31833  axtgupdim2ALTV  31941  dfrdg4  33414  fvray  33604  linedegen  33606  fvline  33607  linethru  33616  hilbert1.1  33617  knoppndvlem21  33873  poimirlem1  34895  hlsuprexch  36519  3dim1lem5  36604  llni2  36650  lplni2  36675  2llnjN  36705  lvoli2  36719  2lplnj  36758  islinei  36878  cdleme40n  37606  cdlemg33b  37845  ax6e2ndeq  40900  ax6e2ndeqVD  41250  ax6e2ndeqALT  41272  refsum2cnlem1  41301  stoweidlem43  42335  nnfoctbdjlem  42744  elprneb  43271  ichnreuop  43641  inlinecirc02plem  44780