Theorem neeq2 2992

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ≠ wne 2929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ne 2930

This theorem is referenced by:  psseq2  4040  prproe  4858  fprg  7097  f1dom3el3dif  7212  f1ounsn  7215  f1prex  7227  resf1extb  7873  xpord2lem  8081  xpord3lem  8088  dfac5  10031  kmlem4  10056  kmlem14  10066  1re  11123  hashge2el2difr  14395  hashdmpropge2  14397  dvdsle  16228  sgrp2rid2ex  18843  isirred  20346  isnzr2  20442  dmatelnd  22431  mdetdiaglem  22533  mdetunilem1  22547  mdetunilem2  22548  maducoeval2  22575  hausnei  23263  regr1lem2  23675  xrhmeo  24891  axtg5seg  28463  axtgupdim2  28469  axtgeucl  28470  ishlg  28600  tglnpt2  28639  axlowdim1  28958  umgrvad2edg  29212  2pthdlem1  29929  3pthdlem1  30165  upgr3v3e3cycl  30181  upgr4cycl4dv4e  30186  eupth2lem3lem4  30232  3cyclfrgrrn1  30286  4cycl2vnunb  30291  numclwwlkovh  30374  numclwwlkovq  30375  numclwwlk2lem1  30377  numclwlk2lem2f  30378  superpos  32355  constrconj  33830  constrcccllem  33839  constrcbvlem  33840  signswch  34646  axtgupdim2ALTV  34753  dfrdg4  36067  fvray  36257  linedegen  36259  fvline  36260  linethru  36269  hilbert1.1  36270  knoppndvlem21  36648  poimirlem1  37734  hlsuprexch  39553  3dim1lem5  39638  llni2  39684  lplni2  39709  2llnjN  39739  lvoli2  39753  2lplnj  39792  islinei  39912  cdleme40n  40640  cdlemg33b  40879  ax6e2ndeq  44716  ax6e2ndeqVD  45065  ax6e2ndeqALT  45087  permac8prim  45171  refsum2cnlem1  45198  stoweidlem43  46203  nnfoctbdjlem  46615  elprneb  47191  ichnreuop  47634  usgrgrtrirex  48112  gpg5nbgrvtx03starlem1  48230  gpg5nbgrvtx03starlem3  48232  gpg5nbgrvtx13starlem1  48233  gpg5nbgrvtx13starlem3  48235  gpg3kgrtriex  48251  inlinecirc02plem  48948  oppcthinendcALT  49602