Theorem neeq2 2995

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

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

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  psseq2  4066  prproe  4881  fprg  7145  f1dom3el3dif  7262  f1ounsn  7265  f1prex  7277  resf1extb  7930  xpord2lem  8141  xpord3lem  8148  dfac5  10143  kmlem4  10168  kmlem14  10178  1re  11235  hashge2el2difr  14499  hashdmpropge2  14501  dvdsle  16329  sgrp2rid2ex  18905  isirred  20379  isnzr2  20478  dmatelnd  22434  mdetdiaglem  22536  mdetunilem1  22550  mdetunilem2  22551  maducoeval2  22578  hausnei  23266  regr1lem2  23678  xrhmeo  24895  axtg5seg  28444  axtgupdim2  28450  axtgeucl  28451  ishlg  28581  tglnpt2  28620  axlowdim1  28938  umgrvad2edg  29192  2pthdlem1  29912  3pthdlem1  30145  upgr3v3e3cycl  30161  upgr4cycl4dv4e  30166  eupth2lem3lem4  30212  3cyclfrgrrn1  30266  4cycl2vnunb  30271  numclwwlkovh  30354  numclwwlkovq  30355  numclwwlk2lem1  30357  numclwlk2lem2f  30358  superpos  32335  constrconj  33779  constrcccllem  33788  constrcbvlem  33789  signswch  34593  axtgupdim2ALTV  34700  dfrdg4  35969  fvray  36159  linedegen  36161  fvline  36162  linethru  36171  hilbert1.1  36172  knoppndvlem21  36550  poimirlem1  37645  hlsuprexch  39400  3dim1lem5  39485  llni2  39531  lplni2  39556  2llnjN  39586  lvoli2  39600  2lplnj  39639  islinei  39759  cdleme40n  40487  cdlemg33b  40726  ax6e2ndeq  44584  ax6e2ndeqVD  44933  ax6e2ndeqALT  44955  refsum2cnlem1  45061  stoweidlem43  46072  nnfoctbdjlem  46484  elprneb  47058  ichnreuop  47486  usgrgrtrirex  47962  gpg5nbgrvtx03starlem1  48070  gpg5nbgrvtx03starlem3  48072  gpg5nbgrvtx13starlem1  48073  gpg5nbgrvtx13starlem3  48075  gpg3kgrtriex  48091  inlinecirc02plem  48766  oppcthinendcALT  49327