Theorem neeq2 3004

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

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

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 2708

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

This theorem is referenced by:  psseq2  4091  prproe  4905  fprg  7175  f1dom3el3dif  7289  f1ounsn  7292  f1prex  7304  resf1extb  7956  xpord2lem  8167  xpord3lem  8174  dfac5  10169  kmlem4  10194  kmlem14  10204  1re  11261  hashge2el2difr  14520  hashdmpropge2  14522  dvdsle  16347  sgrp2rid2ex  18940  isirred  20419  isnzr2  20518  dmatelnd  22502  mdetdiaglem  22604  mdetunilem1  22618  mdetunilem2  22619  maducoeval2  22646  hausnei  23336  regr1lem2  23748  xrhmeo  24977  axtg5seg  28473  axtgupdim2  28479  axtgeucl  28480  ishlg  28610  tglnpt2  28649  axlowdim1  28974  umgrvad2edg  29230  2pthdlem1  29950  3pthdlem1  30183  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  eupth2lem3lem4  30250  3cyclfrgrrn1  30304  4cycl2vnunb  30309  numclwwlkovh  30392  numclwwlkovq  30393  numclwwlk2lem1  30395  numclwlk2lem2f  30396  superpos  32373  constrconj  33786  signswch  34576  axtgupdim2ALTV  34683  dfrdg4  35952  fvray  36142  linedegen  36144  fvline  36145  linethru  36154  hilbert1.1  36155  knoppndvlem21  36533  poimirlem1  37628  hlsuprexch  39383  3dim1lem5  39468  llni2  39514  lplni2  39539  2llnjN  39569  lvoli2  39583  2lplnj  39622  islinei  39742  cdleme40n  40470  cdlemg33b  40709  ax6e2ndeq  44579  ax6e2ndeqVD  44929  ax6e2ndeqALT  44951  refsum2cnlem1  45042  stoweidlem43  46058  nnfoctbdjlem  46470  elprneb  47041  ichnreuop  47459  usgrgrtrirex  47917  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem3  48029  gpg3kgrtriex  48045  inlinecirc02plem  48707  oppcthinendcALT  49090