Theorem neeq2 3003

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ≠ wne 2939

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-ne 2940

This theorem is referenced by:  psseq2  4053  prproe  4868  fprg  7106  f1dom3el3dif  7221  f1prex  7235  xpord2lem  8079  xpord3lem  8086  dfac5  10073  kmlem4  10098  kmlem14  10108  1re  11164  hashge2el2difr  14392  hashdmpropge2  14394  dvdsle  16203  sgrp2rid2ex  18751  isirred  20144  isnzr2  20207  dmatelnd  21882  mdetdiaglem  21984  mdetunilem1  21998  mdetunilem2  21999  maducoeval2  22026  hausnei  22716  regr1lem2  23128  xrhmeo  24346  axtg5seg  27470  axtgupdim2  27476  axtgeucl  27477  ishlg  27607  tglnpt2  27646  axlowdim1  27971  umgrvad2edg  28224  2pthdlem1  28938  3pthdlem1  29171  upgr3v3e3cycl  29187  upgr4cycl4dv4e  29192  eupth2lem3lem4  29238  3cyclfrgrrn1  29292  4cycl2vnunb  29297  numclwwlkovh  29380  numclwwlkovq  29381  numclwwlk2lem1  29383  numclwlk2lem2f  29384  superpos  31359  signswch  33262  axtgupdim2ALTV  33370  dfrdg4  34612  fvray  34802  linedegen  34804  fvline  34805  linethru  34814  hilbert1.1  34815  knoppndvlem21  35071  poimirlem1  36152  hlsuprexch  37917  3dim1lem5  38002  llni2  38048  lplni2  38073  2llnjN  38103  lvoli2  38117  2lplnj  38156  islinei  38276  cdleme40n  39004  cdlemg33b  39243  ax6e2ndeq  42963  ax6e2ndeqVD  43313  ax6e2ndeqALT  43335  refsum2cnlem1  43364  stoweidlem43  44404  nnfoctbdjlem  44816  elprneb  45383  ichnreuop  45784  inlinecirc02plem  46992