Theorem neeq2 2996

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ≠ wne 2933

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 2709

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

This theorem is referenced by:  psseq2  4045  prproe  4863  fprg  7110  f1dom3el3dif  7225  f1ounsn  7228  f1prex  7240  resf1extb  7886  xpord2lem  8094  xpord3lem  8101  dfac5  10051  kmlem4  10076  kmlem14  10086  1re  11144  hashge2el2difr  14416  hashdmpropge2  14418  dvdsle  16249  sgrp2rid2ex  18864  isirred  20367  isnzr2  20463  dmatelnd  22452  mdetdiaglem  22554  mdetunilem1  22568  mdetunilem2  22569  maducoeval2  22596  hausnei  23284  regr1lem2  23696  xrhmeo  24912  axtg5seg  28549  axtgupdim2  28555  axtgeucl  28556  ishlg  28686  tglnpt2  28725  axlowdim1  29044  umgrvad2edg  29298  2pthdlem1  30015  3pthdlem1  30251  upgr3v3e3cycl  30267  upgr4cycl4dv4e  30272  eupth2lem3lem4  30318  3cyclfrgrrn1  30372  4cycl2vnunb  30377  numclwwlkovh  30460  numclwwlkovq  30461  numclwwlk2lem1  30463  numclwlk2lem2f  30464  superpos  32442  constrconj  33923  constrcccllem  33932  constrcbvlem  33933  signswch  34739  axtgupdim2ALTV  34846  dfrdg4  36167  fvray  36357  linedegen  36359  fvline  36360  linethru  36369  hilbert1.1  36370  knoppndvlem21  36754  poimirlem1  37872  hlsuprexch  39757  3dim1lem5  39842  llni2  39888  lplni2  39913  2llnjN  39943  lvoli2  39957  2lplnj  39996  islinei  40116  cdleme40n  40844  cdlemg33b  41083  ax6e2ndeq  44915  ax6e2ndeqVD  45264  ax6e2ndeqALT  45286  permac8prim  45370  refsum2cnlem1  45397  stoweidlem43  46401  nnfoctbdjlem  46813  elprneb  47389  ichnreuop  47832  usgrgrtrirex  48310  gpg5nbgrvtx03starlem1  48428  gpg5nbgrvtx03starlem3  48430  gpg5nbgrvtx13starlem1  48431  gpg5nbgrvtx13starlem3  48433  gpg3kgrtriex  48449  inlinecirc02plem  49146  oppcthinendcALT  49800