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 1542   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

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

This theorem is referenced by:  psseq2  4031  prproe  4848  fprg  7109  f1dom3el3dif  7224  f1ounsn  7227  f1prex  7239  resf1extb  7885  xpord2lem  8092  xpord3lem  8099  dfac5  10051  kmlem4  10076  kmlem14  10086  1re  11144  hashge2el2difr  14443  hashdmpropge2  14445  dvdsle  16279  sgrp2rid2ex  18898  isirred  20399  isnzr2  20495  dmatelnd  22461  mdetdiaglem  22563  mdetunilem1  22577  mdetunilem2  22578  maducoeval2  22605  hausnei  23293  regr1lem2  23705  xrhmeo  24913  axtg5seg  28533  axtgupdim2  28539  axtgeucl  28540  ishlg  28670  tglnpt2  28709  axlowdim1  29028  umgrvad2edg  29282  2pthdlem1  29998  3pthdlem1  30234  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  eupth2lem3lem4  30301  3cyclfrgrrn1  30355  4cycl2vnunb  30360  numclwwlkovh  30443  numclwwlkovq  30444  numclwwlk2lem1  30446  numclwlk2lem2f  30447  superpos  32425  constrconj  33889  constrcccllem  33898  constrcbvlem  33899  signswch  34705  axtgupdim2ALTV  34812  dfrdg4  36133  fvray  36323  linedegen  36325  fvline  36326  linethru  36335  hilbert1.1  36336  knoppndvlem21  36792  qdiff  37641  poimirlem1  37942  hlsuprexch  39827  3dim1lem5  39912  llni2  39958  lplni2  39983  2llnjN  40013  lvoli2  40027  2lplnj  40066  islinei  40186  cdleme40n  40914  cdlemg33b  41153  ax6e2ndeq  44986  ax6e2ndeqVD  45335  ax6e2ndeqALT  45357  permac8prim  45441  refsum2cnlem1  45468  stoweidlem43  46471  nnfoctbdjlem  46883  elprneb  47477  ichnreuop  47932  usgrgrtrirex  48426  gpg5nbgrvtx03starlem1  48544  gpg5nbgrvtx03starlem3  48546  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem3  48549  gpg3kgrtriex  48565  inlinecirc02plem  49262  oppcthinendcALT  49916