Theorem neeq2 3079

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

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

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 2793

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

This theorem is referenced by:  psseq2  4065  prproe  4836  fprg  6917  f1dom3el3dif  7027  f1prex  7040  dfac5  9554  kmlem4  9579  kmlem14  9589  1re  10641  hashge2el2difr  13840  hashdmpropge2  13842  dvdsle  15660  sgrp2rid2ex  18092  isirred  19449  isnzr2  20036  dmatelnd  21105  mdetdiaglem  21207  mdetunilem1  21221  mdetunilem2  21222  maducoeval2  21249  hausnei  21936  regr1lem2  22348  xrhmeo  23550  axtg5seg  26251  axtgupdim2  26257  axtgeucl  26258  ishlg  26388  tglnpt2  26427  axlowdim1  26745  umgrvad2edg  26995  2pthdlem1  27709  3pthdlem1  27943  upgr3v3e3cycl  27959  upgr4cycl4dv4e  27964  eupth2lem3lem4  28010  3cyclfrgrrn1  28064  4cycl2vnunb  28069  numclwwlkovh  28152  numclwwlkovq  28153  numclwwlk2lem1  28155  numclwlk2lem2f  28156  superpos  30131  signswch  31831  axtgupdim2ALTV  31939  dfrdg4  33412  fvray  33602  linedegen  33604  fvline  33605  linethru  33614  hilbert1.1  33615  knoppndvlem21  33871  poimirlem1  34908  hlsuprexch  36532  3dim1lem5  36617  llni2  36663  lplni2  36688  2llnjN  36718  lvoli2  36732  2lplnj  36771  islinei  36891  cdleme40n  37619  cdlemg33b  37858  ax6e2ndeq  40913  ax6e2ndeqVD  41263  ax6e2ndeqALT  41285  refsum2cnlem1  41314  stoweidlem43  42348  nnfoctbdjlem  42757  elprneb  43284  ichnreuop  43654  inlinecirc02plem  44793