Theorem neeq2 2989

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

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

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 2702

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

This theorem is referenced by:  psseq2  4057  prproe  4872  fprg  7130  f1dom3el3dif  7247  f1ounsn  7250  f1prex  7262  resf1extb  7913  xpord2lem  8124  xpord3lem  8131  dfac5  10089  kmlem4  10114  kmlem14  10124  1re  11181  hashge2el2difr  14453  hashdmpropge2  14455  dvdsle  16287  sgrp2rid2ex  18861  isirred  20335  isnzr2  20434  dmatelnd  22390  mdetdiaglem  22492  mdetunilem1  22506  mdetunilem2  22507  maducoeval2  22534  hausnei  23222  regr1lem2  23634  xrhmeo  24851  axtg5seg  28399  axtgupdim2  28405  axtgeucl  28406  ishlg  28536  tglnpt2  28575  axlowdim1  28893  umgrvad2edg  29147  2pthdlem1  29867  3pthdlem1  30100  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  eupth2lem3lem4  30167  3cyclfrgrrn1  30221  4cycl2vnunb  30226  numclwwlkovh  30309  numclwwlkovq  30310  numclwwlk2lem1  30312  numclwlk2lem2f  30313  superpos  32290  constrconj  33742  constrcccllem  33751  constrcbvlem  33752  signswch  34559  axtgupdim2ALTV  34666  dfrdg4  35946  fvray  36136  linedegen  36138  fvline  36139  linethru  36148  hilbert1.1  36149  knoppndvlem21  36527  poimirlem1  37622  hlsuprexch  39382  3dim1lem5  39467  llni2  39513  lplni2  39538  2llnjN  39568  lvoli2  39582  2lplnj  39621  islinei  39741  cdleme40n  40469  cdlemg33b  40708  ax6e2ndeq  44556  ax6e2ndeqVD  44905  ax6e2ndeqALT  44927  permac8prim  45011  refsum2cnlem1  45038  stoweidlem43  46048  nnfoctbdjlem  46460  elprneb  47034  ichnreuop  47477  usgrgrtrirex  47953  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem3  48068  gpg3kgrtriex  48084  inlinecirc02plem  48779  oppcthinendcALT  49434