Theorem neeq2 2995

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ne 2933

This theorem is referenced by:  psseq2  4043  prproe  4861  fprg  7100  f1dom3el3dif  7215  f1ounsn  7218  f1prex  7230  resf1extb  7876  xpord2lem  8084  xpord3lem  8091  dfac5  10039  kmlem4  10064  kmlem14  10074  1re  11132  hashge2el2difr  14404  hashdmpropge2  14406  dvdsle  16237  sgrp2rid2ex  18852  isirred  20355  isnzr2  20451  dmatelnd  22440  mdetdiaglem  22542  mdetunilem1  22556  mdetunilem2  22557  maducoeval2  22584  hausnei  23272  regr1lem2  23684  xrhmeo  24900  axtg5seg  28537  axtgupdim2  28543  axtgeucl  28544  ishlg  28674  tglnpt2  28713  axlowdim1  29032  umgrvad2edg  29286  2pthdlem1  30003  3pthdlem1  30239  upgr3v3e3cycl  30255  upgr4cycl4dv4e  30260  eupth2lem3lem4  30306  3cyclfrgrrn1  30360  4cycl2vnunb  30365  numclwwlkovh  30448  numclwwlkovq  30449  numclwwlk2lem1  30451  numclwlk2lem2f  30452  superpos  32429  constrconj  33902  constrcccllem  33911  constrcbvlem  33912  signswch  34718  axtgupdim2ALTV  34825  dfrdg4  36145  fvray  36335  linedegen  36337  fvline  36338  linethru  36347  hilbert1.1  36348  knoppndvlem21  36732  poimirlem1  37822  hlsuprexch  39641  3dim1lem5  39726  llni2  39772  lplni2  39797  2llnjN  39827  lvoli2  39841  2lplnj  39880  islinei  40000  cdleme40n  40728  cdlemg33b  40967  ax6e2ndeq  44800  ax6e2ndeqVD  45149  ax6e2ndeqALT  45171  permac8prim  45255  refsum2cnlem1  45282  stoweidlem43  46287  nnfoctbdjlem  46699  elprneb  47275  ichnreuop  47718  usgrgrtrirex  48196  gpg5nbgrvtx03starlem1  48314  gpg5nbgrvtx03starlem3  48316  gpg5nbgrvtx13starlem1  48317  gpg5nbgrvtx13starlem3  48319  gpg3kgrtriex  48335  inlinecirc02plem  49032  oppcthinendcALT  49686