Theorem neeq2 3023

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ne 2961

This theorem is used by:  psseq2  4046  prproe  4872  fprg  7156  f1dom3el3dif  7269  f1ounsn  7276  f1prex  7288  resf1extb  7933  xpord2lem  8140  xpord3lem  8147  dfac5  10124  kmlem4  10149  kmlem14  10159  1re  11219  hashge2el2difr  14532  hashdmpropge2  14534  dvdsle  16386  sgrp2rid2ex  19013  isirred  20527  isnzr2  20645  dmatelnd  22683  mdetdiaglem  22785  mdetunilem1  22799  mdetunilem2  22800  maducoeval2  22827  hausnei  23515  regr1lem2  23928  xrhmeo  25136  axtg5seg  28765  axtgupdim2  28771  axtgeucl  28772  ishlg2  28902  ishlg  28905  tglnpt2  28957  axlowdim1  29340  umgrvad2edg  29597  2pthdlem1  30322  3pthdlem1  30562  upgr3v3e3cycl  30578  upgr4cycl4dv4e  30583  eupth2lem3lem4  30629  3cyclfrgrrn1  30683  4cycl2vnunb  30688  numclwwlkovh  30771  numclwwlkovq  30772  numclwwlk2lem1  30774  numclwlk2lem2f  30775  superpos  32753  constrconj  34175  constrcccllem  34184  constrcbvlem  34185  signswch  34989  axtgupdim2ALTV  35096  dfrdg4  36456  fvray  36646  linedegen  36648  fvline  36649  linethru  36658  hilbert1.1  36659  knoppndvlem21  37154  qdiff  38004  poimirlem1  38305  hlsuprexch  40188  3dim1lem5  40273  llni2  40319  lplni2  40344  2llnjN  40374  lvoli2  40388  2lplnj  40427  islinei  40547  cdleme40n  41275  cdlemg33b  41514  ax6e2ndeq  45301  ax6e2ndeqVD  45650  ax6e2ndeqALT  45672  permac8prim  45756  refsum2cnlem1  45790  stoweidlem43  46790  nnfoctbdjlem  47202  elprneb  47799  ichnreuop  48254  usgrgrtrirex  48748  gpg5nbgrvtx03starlem1  48866  gpg5nbgrvtx03starlem3  48868  gpg5nbgrvtx13starlem1  48869  gpg5nbgrvtx13starlem3  48871  gpg3kgrtriex  48887  inlinecirc02plem  49599  oppcthinendcALT  50252