Theorem neeq2 2845

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ≠ wne 2780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782

This theorem is referenced by:  psseq2  3657  fprg  6327  f1dom3el3dif  6426  f1prex  6439  dfac5  8834  kmlem4  8858  kmlem14  8868  1re  9918  hashge2el2difr  13118  dvdsle  14870  sgrp2rid2ex  17237  isirred  18522  isnzr2  19084  dmatelnd  20121  mdetdiaglem  20223  mdetunilem1  20237  mdetunilem2  20238  maducoeval2  20265  hausnei  20942  regr1lem2  21353  xrhmeo  22553  axtg5seg  25164  axtgupdim2  25170  axtgeucl  25171  ishlg  25297  tglnpt2  25336  axlowdim1  25639  structgrssvtxlem  25700  2pthoncl  26133  clwlknclwlkdifs  26487  3cyclfrgrarn1  26539  4cycl2vnunb  26544  numclwwlk2lem1  26629  numclwlk2lem2f  26630  superpos  28597  signswch  29964  axtgupdim2OLD  29999  dfrdg4  31228  fvray  31418  linedegen  31420  fvline  31421  linethru  31430  hilbert1.1  31431  knoppndvlem21  31693  poimirlem1  32580  hlsuprexch  33685  3dim1lem5  33770  llni2  33816  lplni2  33841  2llnjN  33871  lvoli2  33885  2lplnj  33924  islinei  34044  cdleme40n  34774  cdlemg33b  35013  ax6e2ndeq  37796  ax6e2ndeqVD  38167  ax6e2ndeqALT  38189  refsum2cnlem1  38219  stoweidlem43  38936  nnfoctbdjlem  39348  elprneb  39939  umgrvad2edg  40440  2pthdlem1  41137  clwwlknclwwlkdifs  41181  3pthdlem1  41331  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352  eupth2lem3lem4  41399  3cyclfrgrrn1  41455  4cycl2vnunb-av  41460  av-numclwwlkovq  41529  av-numclwwlk2lem1  41532  av-numclwlk2lem2f  41533