Theorem neeq2 3005

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ≠ wne 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2942

This theorem is referenced by:  psseq2  4089  prproe  4907  fprg  7153  f1dom3el3dif  7268  f1prex  7282  xpord2lem  8128  xpord3lem  8135  dfac5  10123  kmlem4  10148  kmlem14  10158  1re  11214  hashge2el2difr  14442  hashdmpropge2  14444  dvdsle  16253  sgrp2rid2ex  18808  isirred  20233  isnzr2  20297  dmatelnd  21998  mdetdiaglem  22100  mdetunilem1  22114  mdetunilem2  22115  maducoeval2  22142  hausnei  22832  regr1lem2  23244  xrhmeo  24462  axtg5seg  27716  axtgupdim2  27722  axtgeucl  27723  ishlg  27853  tglnpt2  27892  axlowdim1  28217  umgrvad2edg  28470  2pthdlem1  29184  3pthdlem1  29417  upgr3v3e3cycl  29433  upgr4cycl4dv4e  29438  eupth2lem3lem4  29484  3cyclfrgrrn1  29538  4cycl2vnunb  29543  numclwwlkovh  29626  numclwwlkovq  29627  numclwwlk2lem1  29629  numclwlk2lem2f  29630  superpos  31607  signswch  33572  axtgupdim2ALTV  33680  dfrdg4  34923  fvray  35113  linedegen  35115  fvline  35116  linethru  35125  hilbert1.1  35126  knoppndvlem21  35408  poimirlem1  36489  hlsuprexch  38252  3dim1lem5  38337  llni2  38383  lplni2  38408  2llnjN  38438  lvoli2  38452  2lplnj  38491  islinei  38611  cdleme40n  39339  cdlemg33b  39578  ax6e2ndeq  43320  ax6e2ndeqVD  43670  ax6e2ndeqALT  43692  refsum2cnlem1  43721  stoweidlem43  44759  nnfoctbdjlem  45171  elprneb  45739  ichnreuop  46140  inlinecirc02plem  47472