Theorem neeq2 3001

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536   ≠ wne 2937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ne 2938

This theorem is referenced by:  psseq2  4100  prproe  4909  fprg  7174  f1dom3el3dif  7288  f1ounsn  7291  f1prex  7303  xpord2lem  8165  xpord3lem  8172  dfac5  10166  kmlem4  10191  kmlem14  10201  1re  11258  hashge2el2difr  14516  hashdmpropge2  14518  dvdsle  16343  sgrp2rid2ex  18952  isirred  20435  isnzr2  20534  dmatelnd  22517  mdetdiaglem  22619  mdetunilem1  22633  mdetunilem2  22634  maducoeval2  22661  hausnei  23351  regr1lem2  23763  xrhmeo  24990  axtg5seg  28487  axtgupdim2  28493  axtgeucl  28494  ishlg  28624  tglnpt2  28663  axlowdim1  28988  umgrvad2edg  29244  2pthdlem1  29959  3pthdlem1  30192  upgr3v3e3cycl  30208  upgr4cycl4dv4e  30213  eupth2lem3lem4  30259  3cyclfrgrrn1  30313  4cycl2vnunb  30318  numclwwlkovh  30401  numclwwlkovq  30402  numclwwlk2lem1  30404  numclwlk2lem2f  30405  superpos  32382  constrconj  33749  signswch  34554  axtgupdim2ALTV  34661  dfrdg4  35932  fvray  36122  linedegen  36124  fvline  36125  linethru  36134  hilbert1.1  36135  knoppndvlem21  36514  poimirlem1  37607  hlsuprexch  39363  3dim1lem5  39448  llni2  39494  lplni2  39519  2llnjN  39549  lvoli2  39563  2lplnj  39602  islinei  39722  cdleme40n  40450  cdlemg33b  40689  ax6e2ndeq  44556  ax6e2ndeqVD  44906  ax6e2ndeqALT  44928  refsum2cnlem1  44974  stoweidlem43  45998  nnfoctbdjlem  46410  elprneb  46978  ichnreuop  47396  usgrgrtrirex  47852  gpg5nbgrvtx03starlem1  47958  gpg5nbgrvtx03starlem3  47960  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem3  47963  inlinecirc02plem  48635