Theorem neeq2 3006

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ≠ wne 2942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-ne 2943

This theorem is referenced by:  psseq2  4019  prproe  4834  fprg  7009  f1dom3el3dif  7123  f1prex  7136  dfac5  9815  kmlem4  9840  kmlem14  9850  1re  10906  hashge2el2difr  14123  hashdmpropge2  14125  dvdsle  15947  sgrp2rid2ex  18481  isirred  19856  isnzr2  20447  dmatelnd  21553  mdetdiaglem  21655  mdetunilem1  21669  mdetunilem2  21670  maducoeval2  21697  hausnei  22387  regr1lem2  22799  xrhmeo  24015  axtg5seg  26730  axtgupdim2  26736  axtgeucl  26737  ishlg  26867  tglnpt2  26906  axlowdim1  27230  umgrvad2edg  27483  2pthdlem1  28196  3pthdlem1  28429  upgr3v3e3cycl  28445  upgr4cycl4dv4e  28450  eupth2lem3lem4  28496  3cyclfrgrrn1  28550  4cycl2vnunb  28555  numclwwlkovh  28638  numclwwlkovq  28639  numclwwlk2lem1  28641  numclwlk2lem2f  28642  superpos  30617  signswch  32440  axtgupdim2ALTV  32548  xpord2lem  33716  xpord3lem  33722  dfrdg4  34180  fvray  34370  linedegen  34372  fvline  34373  linethru  34382  hilbert1.1  34383  knoppndvlem21  34639  poimirlem1  35705  hlsuprexch  37322  3dim1lem5  37407  llni2  37453  lplni2  37478  2llnjN  37508  lvoli2  37522  2lplnj  37561  islinei  37681  cdleme40n  38409  cdlemg33b  38648  ax6e2ndeq  42068  ax6e2ndeqVD  42418  ax6e2ndeqALT  42440  refsum2cnlem1  42469  stoweidlem43  43474  nnfoctbdjlem  43883  elprneb  44410  ichnreuop  44812  inlinecirc02plem  46020