Theorem neeq2 3007

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ≠ wne 2943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-ne 2944

This theorem is referenced by:  psseq2  4023  prproe  4837  fprg  7027  f1dom3el3dif  7142  f1prex  7156  dfac5  9884  kmlem4  9909  kmlem14  9919  1re  10975  hashge2el2difr  14195  hashdmpropge2  14197  dvdsle  16019  sgrp2rid2ex  18566  isirred  19941  isnzr2  20534  dmatelnd  21645  mdetdiaglem  21747  mdetunilem1  21761  mdetunilem2  21762  maducoeval2  21789  hausnei  22479  regr1lem2  22891  xrhmeo  24109  axtg5seg  26826  axtgupdim2  26832  axtgeucl  26833  ishlg  26963  tglnpt2  27002  axlowdim1  27327  umgrvad2edg  27580  2pthdlem1  28295  3pthdlem1  28528  upgr3v3e3cycl  28544  upgr4cycl4dv4e  28549  eupth2lem3lem4  28595  3cyclfrgrrn1  28649  4cycl2vnunb  28654  numclwwlkovh  28737  numclwwlkovq  28738  numclwwlk2lem1  28740  numclwlk2lem2f  28741  superpos  30716  signswch  32540  axtgupdim2ALTV  32648  xpord2lem  33789  xpord3lem  33795  dfrdg4  34253  fvray  34443  linedegen  34445  fvline  34446  linethru  34455  hilbert1.1  34456  knoppndvlem21  34712  poimirlem1  35778  hlsuprexch  37395  3dim1lem5  37480  llni2  37526  lplni2  37551  2llnjN  37581  lvoli2  37595  2lplnj  37634  islinei  37754  cdleme40n  38482  cdlemg33b  38721  ax6e2ndeq  42179  ax6e2ndeqVD  42529  ax6e2ndeqALT  42551  refsum2cnlem1  42580  stoweidlem43  43584  nnfoctbdjlem  43993  elprneb  44523  ichnreuop  44924  inlinecirc02plem  46132