Theorem neeq2 3032

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1601   ≠ wne 2969

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2770  df-ne 2970

This theorem is referenced by:  psseq2  3917  prproe  4671  fprg  6690  f1dom3el3dif  6800  f1prex  6813  dfac5  9286  kmlem4  9312  kmlem14  9322  1re  10378  hashge2el2difr  13581  hashdmpropge2  13583  dvdsle  15443  sgrp2rid2ex  17805  isirred  19090  isnzr2  19664  dmatelnd  20711  mdetdiaglem  20813  mdetunilem1  20827  mdetunilem2  20828  maducoeval2  20855  hausnei  21544  regr1lem2  21956  xrhmeo  23157  axtg5seg  25820  axtgupdim2  25826  axtgeucl  25827  ishlg  25957  tglnpt2  25996  axlowdim1  26312  umgrvad2edg  26563  2pthdlem1  27314  3pthdlem1  27571  upgr3v3e3cycl  27587  upgr4cycl4dv4e  27592  eupth2lem3lem4  27639  3cyclfrgrrn1  27697  4cycl2vnunb  27702  numclwwlkovh  27805  numclwwlkovq  27806  numclwwlk2lem1  27808  numclwlk2lem2f  27809  numclwlk2lem2fOLD  27812  superpos  29789  signswch  31242  axtgupdim2OLD  31352  dfrdg4  32651  fvray  32841  linedegen  32843  fvline  32844  linethru  32853  hilbert1.1  32854  knoppndvlem21  33109  poimirlem1  34041  hlsuprexch  35540  3dim1lem5  35625  llni2  35671  lplni2  35696  2llnjN  35726  lvoli2  35740  2lplnj  35779  islinei  35899  cdleme40n  36627  cdlemg33b  36866  ax6e2ndeq  39729  ax6e2ndeqVD  40088  ax6e2ndeqALT  40110  refsum2cnlem1  40139  stoweidlem43  41197  nnfoctbdjlem  41606  elprneb  42108  inlinecirc02plem  43532