Theorem neeq2 2988

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

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

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 2701

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

This theorem is referenced by:  psseq2  4054  prproe  4869  fprg  7127  f1dom3el3dif  7244  f1ounsn  7247  f1prex  7259  resf1extb  7910  xpord2lem  8121  xpord3lem  8128  dfac5  10082  kmlem4  10107  kmlem14  10117  1re  11174  hashge2el2difr  14446  hashdmpropge2  14448  dvdsle  16280  sgrp2rid2ex  18854  isirred  20328  isnzr2  20427  dmatelnd  22383  mdetdiaglem  22485  mdetunilem1  22499  mdetunilem2  22500  maducoeval2  22527  hausnei  23215  regr1lem2  23627  xrhmeo  24844  axtg5seg  28392  axtgupdim2  28398  axtgeucl  28399  ishlg  28529  tglnpt2  28568  axlowdim1  28886  umgrvad2edg  29140  2pthdlem1  29860  3pthdlem1  30093  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  eupth2lem3lem4  30160  3cyclfrgrrn1  30214  4cycl2vnunb  30219  numclwwlkovh  30302  numclwwlkovq  30303  numclwwlk2lem1  30305  numclwlk2lem2f  30306  superpos  32283  constrconj  33735  constrcccllem  33744  constrcbvlem  33745  signswch  34552  axtgupdim2ALTV  34659  dfrdg4  35939  fvray  36129  linedegen  36131  fvline  36132  linethru  36141  hilbert1.1  36142  knoppndvlem21  36520  poimirlem1  37615  hlsuprexch  39375  3dim1lem5  39460  llni2  39506  lplni2  39531  2llnjN  39561  lvoli2  39575  2lplnj  39614  islinei  39734  cdleme40n  40462  cdlemg33b  40701  ax6e2ndeq  44549  ax6e2ndeqVD  44898  ax6e2ndeqALT  44920  permac8prim  45004  refsum2cnlem1  45031  stoweidlem43  46041  nnfoctbdjlem  46453  elprneb  47030  ichnreuop  47473  usgrgrtrirex  47949  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem3  48064  gpg3kgrtriex  48080  inlinecirc02plem  48775  oppcthinendcALT  49430