Theorem neeq2 2997

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ≠ wne 2934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ne 2935

This theorem is referenced by:  psseq2  4022  prproe  4836  fprg  7098  f1dom3el3dif  7213  f1ounsn  7216  f1prex  7228  resf1extb  7874  xpord2lem  8082  xpord3lem  8089  dfac5  10042  kmlem4  10067  kmlem14  10077  1re  11135  hashge2el2difr  14434  hashdmpropge2  14436  dvdsle  16270  sgrp2rid2ex  18889  isirred  20390  isnzr2  20490  dmatelnd  22479  mdetdiaglem  22581  mdetunilem1  22595  mdetunilem2  22596  maducoeval2  22623  hausnei  23311  regr1lem2  23723  xrhmeo  24931  axtg5seg  28551  axtgupdim2  28557  axtgeucl  28558  ishlg  28688  tglnpt2  28727  axlowdim1  29046  umgrvad2edg  29300  2pthdlem1  30016  3pthdlem1  30252  upgr3v3e3cycl  30268  upgr4cycl4dv4e  30273  eupth2lem3lem4  30319  3cyclfrgrrn1  30373  4cycl2vnunb  30378  numclwwlkovh  30461  numclwwlkovq  30462  numclwwlk2lem1  30464  numclwlk2lem2f  30465  superpos  32443  constrconj  33929  constrcccllem  33938  constrcbvlem  33939  signswch  34745  axtgupdim2ALTV  34852  dfrdg4  36179  fvray  36369  linedegen  36371  fvline  36372  linethru  36381  hilbert1.1  36382  knoppndvlem21  36838  qdiff  37687  poimirlem1  37988  hlsuprexch  39873  3dim1lem5  39958  llni2  40004  lplni2  40029  2llnjN  40059  lvoli2  40073  2lplnj  40112  islinei  40232  cdleme40n  40960  cdlemg33b  41199  ax6e2ndeq  45003  ax6e2ndeqVD  45352  ax6e2ndeqALT  45374  permac8prim  45458  refsum2cnlem1  45485  stoweidlem43  46486  nnfoctbdjlem  46898  elprneb  47492  ichnreuop  47947  usgrgrtrirex  48441  gpg5nbgrvtx03starlem1  48559  gpg5nbgrvtx03starlem3  48561  gpg5nbgrvtx13starlem1  48562  gpg5nbgrvtx13starlem3  48564  gpg3kgrtriex  48580  inlinecirc02plem  49277  oppcthinendcALT  49931