Theorem neeq2 3018

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 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	neeq2d 3015	1 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ne 2956

This theorem is used by:  psseq2  4018  prproe  4832  fprg  7160  f1dom3el3dif  7274  f1ounsn  7281  f1prex  7293  resf1extb  7947  xpord2lem  8162  xpord3lem  8169  dfac5  10211  kmlem4  10236  kmlem14  10246  1re  11312  hashge2el2difr  14630  hashdmpropge2  14632  dvdsle  16486  sgrp2rid2ex  19132  isirred  20655  isnzr2  20774  dmatelnd  22817  mdetdiaglem  22919  mdetunilem1  22933  mdetunilem2  22934  maducoeval2  22961  hausnei  23652  regr1lem2  24065  xrhmeo  25273  axtg5seg  28933  axtgupdim2  28939  axtgeucl  28940  ishlg2  29071  ishlg  29074  tglnpt2  29127  elcgrabasi  29381  axlowdim1  29543  umgrvad2edg  29800  2pthdlem1  30525  3pthdlem1  30771  upgr3v3e3cycl  30787  upgr4cycl4dv4e  30792  eupth2lem3lem4  30838  3cyclfrgrrn1  30892  4cycl2vnunb  30897  numclwwlkovh  30980  numclwwlkovq  30981  numclwwlk2lem1  30983  numclwlk2lem2f  30984  superpos  32962  constrconj  34424  constrcccllem  34433  constrcbvlem  34434  signswch  35237  axtgupdim2ALTV  35344  dfrdg4  36808  fvray  36999  linedegen  37001  fvline  37002  linethru  37011  hilbert1.1  37012  knoppndvlem21  37491  qdiff  38342  poimirlem1  38633  hlsuprexch  40532  3dim1lem5  40617  llni2  40663  lplni2  40688  2llnjN  40718  lvoli2  40732  2lplnj  40771  islinei  40891  cdleme40n  41619  cdlemg33b  41858  ax6e2ndeq  45636  ax6e2ndeqVD  45985  ax6e2ndeqALT  46007  permac8prim  46098  refsum2cnlem1  46148  stoweidlem43  47147  nnfoctbdjlem  47559  elprneb  48193  ichnreuop  48648  usgrgrtrirex  49142  gpg5nbgrvtx03starlem1  49260  gpg5nbgrvtx03starlem3  49262  gpg5nbgrvtx13starlem1  49263  gpg5nbgrvtx13starlem3  49265  gpg3kgrtriex  49281  inlinecirc02plem  49992  oppcthinendcALT  50670