Theorem neeq2 2988

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  psseq2  4044  prproe  4859  fprg  7093  f1dom3el3dif  7210  f1ounsn  7213  f1prex  7225  resf1extb  7874  xpord2lem  8082  xpord3lem  8089  dfac5  10042  kmlem4  10067  kmlem14  10077  1re  11134  hashge2el2difr  14407  hashdmpropge2  14409  dvdsle  16240  sgrp2rid2ex  18820  isirred  20323  isnzr2  20422  dmatelnd  22400  mdetdiaglem  22502  mdetunilem1  22516  mdetunilem2  22517  maducoeval2  22544  hausnei  23232  regr1lem2  23644  xrhmeo  24861  axtg5seg  28429  axtgupdim2  28435  axtgeucl  28436  ishlg  28566  tglnpt2  28605  axlowdim1  28923  umgrvad2edg  29177  2pthdlem1  29894  3pthdlem1  30127  upgr3v3e3cycl  30143  upgr4cycl4dv4e  30148  eupth2lem3lem4  30194  3cyclfrgrrn1  30248  4cycl2vnunb  30253  numclwwlkovh  30336  numclwwlkovq  30337  numclwwlk2lem1  30339  numclwlk2lem2f  30340  superpos  32317  constrconj  33731  constrcccllem  33740  constrcbvlem  33741  signswch  34548  axtgupdim2ALTV  34655  dfrdg4  35944  fvray  36134  linedegen  36136  fvline  36137  linethru  36146  hilbert1.1  36147  knoppndvlem21  36525  poimirlem1  37620  hlsuprexch  39380  3dim1lem5  39465  llni2  39511  lplni2  39536  2llnjN  39566  lvoli2  39580  2lplnj  39619  islinei  39739  cdleme40n  40467  cdlemg33b  40706  ax6e2ndeq  44553  ax6e2ndeqVD  44902  ax6e2ndeqALT  44924  permac8prim  45008  refsum2cnlem1  45035  stoweidlem43  46044  nnfoctbdjlem  46456  elprneb  47033  ichnreuop  47476  usgrgrtrirex  47954  gpg5nbgrvtx03starlem1  48072  gpg5nbgrvtx03starlem3  48074  gpg5nbgrvtx13starlem1  48075  gpg5nbgrvtx13starlem3  48077  gpg3kgrtriex  48093  inlinecirc02plem  48791  oppcthinendcALT  49446