Theorem neeq2 3019

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

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

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 2155  ax-ext 2733

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

This theorem is used by:  psseq2  4039  prproe  4865  fprg  7157  f1dom3el3dif  7271  f1ounsn  7278  f1prex  7290  resf1extb  7944  xpord2lem  8152  xpord3lem  8159  dfac5  10200  kmlem4  10225  kmlem14  10235  1re  11301  hashge2el2difr  14619  hashdmpropge2  14621  dvdsle  16473  sgrp2rid2ex  19119  isirred  20642  isnzr2  20761  dmatelnd  22804  mdetdiaglem  22906  mdetunilem1  22920  mdetunilem2  22921  maducoeval2  22948  hausnei  23639  regr1lem2  24052  xrhmeo  25260  axtg5seg  28920  axtgupdim2  28926  axtgeucl  28927  ishlg2  29058  ishlg  29061  tglnpt2  29114  elcgrabasi  29368  axlowdim1  29530  umgrvad2edg  29787  2pthdlem1  30512  3pthdlem1  30758  upgr3v3e3cycl  30774  upgr4cycl4dv4e  30779  eupth2lem3lem4  30825  3cyclfrgrrn1  30879  4cycl2vnunb  30884  numclwwlkovh  30967  numclwwlkovq  30968  numclwwlk2lem1  30970  numclwlk2lem2f  30971  superpos  32949  constrconj  34370  constrcccllem  34379  constrcbvlem  34380  signswch  35183  axtgupdim2ALTV  35290  dfrdg4  36695  fvray  36886  linedegen  36888  fvline  36889  linethru  36898  hilbert1.1  36899  knoppndvlem21  37378  qdiff  38228  poimirlem1  38519  hlsuprexch  40418  3dim1lem5  40503  llni2  40549  lplni2  40574  2llnjN  40604  lvoli2  40618  2lplnj  40657  islinei  40777  cdleme40n  41505  cdlemg33b  41744  ax6e2ndeq  45527  ax6e2ndeqVD  45876  ax6e2ndeqALT  45898  permac8prim  45982  refsum2cnlem1  46023  stoweidlem43  47022  nnfoctbdjlem  47434  elprneb  48068  ichnreuop  48523  usgrgrtrirex  49017  gpg5nbgrvtx03starlem1  49135  gpg5nbgrvtx03starlem3  49137  gpg5nbgrvtx13starlem1  49138  gpg5nbgrvtx13starlem3  49140  gpg3kgrtriex  49156  inlinecirc02plem  49867  oppcthinendcALT  50518