Theorem neeq2 3019

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   ≠ wne 2956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ne 2957

This theorem is referenced by:  psseq2  4042  prproe  4860  fprg  7133  f1dom3el3dif  7248  f1ounsn  7251  f1prex  7263  resf1extb  7910  xpord2lem  8116  xpord3lem  8123  dfac5  10079  kmlem4  10104  kmlem14  10114  1re  11175  hashge2el2difr  14488  hashdmpropge2  14490  dvdsle  16335  sgrp2rid2ex  18955  isirred  20455  isnzr2  20555  dmatelnd  22544  mdetdiaglem  22646  mdetunilem1  22660  mdetunilem2  22661  maducoeval2  22688  hausnei  23376  regr1lem2  23788  xrhmeo  24996  axtg5seg  28622  axtgupdim2  28628  axtgeucl  28629  ishlg  28759  tglnpt2  28798  axlowdim1  29117  umgrvad2edg  29371  2pthdlem1  30087  3pthdlem1  30323  upgr3v3e3cycl  30339  upgr4cycl4dv4e  30344  eupth2lem3lem4  30390  3cyclfrgrrn1  30444  4cycl2vnunb  30449  numclwwlkovh  30532  numclwwlkovq  30533  numclwwlk2lem1  30535  numclwlk2lem2f  30536  superpos  32514  constrconj  34003  constrcccllem  34012  constrcbvlem  34013  signswch  34816  axtgupdim2ALTV  34923  dfrdg4  36262  fvray  36452  linedegen  36454  fvline  36455  linethru  36464  hilbert1.1  36465  knoppndvlem21  36931  qdiff  37780  poimirlem1  38081  hlsuprexch  39966  3dim1lem5  40051  llni2  40097  lplni2  40122  2llnjN  40152  lvoli2  40166  2lplnj  40205  islinei  40325  cdleme40n  41053  cdlemg33b  41292  ax6e2ndeq  45096  ax6e2ndeqVD  45445  ax6e2ndeqALT  45467  permac8prim  45551  refsum2cnlem1  45578  stoweidlem43  46578  nnfoctbdjlem  46990  elprneb  47584  ichnreuop  48039  usgrgrtrirex  48533  gpg5nbgrvtx03starlem1  48651  gpg5nbgrvtx03starlem3  48653  gpg5nbgrvtx13starlem1  48654  gpg5nbgrvtx13starlem3  48656  gpg3kgrtriex  48672  inlinecirc02plem  49369  oppcthinendcALT  50023