Theorem neeq2 3021

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ≠ wne 2958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ne 2959

This theorem is referenced by:  psseq2  4045  prproe  4870  fprg  7152  f1dom3el3dif  7267  f1ounsn  7270  f1prex  7282  resf1extb  7927  xpord2lem  8134  xpord3lem  8141  dfac5  10108  kmlem4  10133  kmlem14  10143  1re  11203  hashge2el2difr  14514  hashdmpropge2  14516  dvdsle  16363  sgrp2rid2ex  18984  isirred  20497  isnzr2  20615  dmatelnd  22653  mdetdiaglem  22755  mdetunilem1  22769  mdetunilem2  22770  maducoeval2  22797  hausnei  23485  regr1lem2  23897  xrhmeo  25105  axtg5seg  28734  axtgupdim2  28740  axtgeucl  28741  ishlg2  28871  ishlg  28874  tglnpt2  28926  axlowdim1  29309  umgrvad2edg  29563  2pthdlem1  30279  3pthdlem1  30515  upgr3v3e3cycl  30531  upgr4cycl4dv4e  30536  eupth2lem3lem4  30582  3cyclfrgrrn1  30636  4cycl2vnunb  30641  numclwwlkovh  30724  numclwwlkovq  30725  numclwwlk2lem1  30727  numclwlk2lem2f  30728  superpos  32706  constrconj  34135  constrcccllem  34144  constrcbvlem  34145  signswch  34948  axtgupdim2ALTV  35055  dfrdg4  36443  fvray  36633  linedegen  36635  fvline  36636  linethru  36645  hilbert1.1  36646  knoppndvlem21  37121  qdiff  37971  poimirlem1  38272  hlsuprexch  40155  3dim1lem5  40240  llni2  40286  lplni2  40311  2llnjN  40341  lvoli2  40355  2lplnj  40394  islinei  40514  cdleme40n  41242  cdlemg33b  41481  ax6e2ndeq  45268  ax6e2ndeqVD  45617  ax6e2ndeqALT  45639  permac8prim  45723  refsum2cnlem1  45757  stoweidlem43  46757  nnfoctbdjlem  47169  elprneb  47766  ichnreuop  48221  usgrgrtrirex  48715  gpg5nbgrvtx03starlem1  48833  gpg5nbgrvtx03starlem3  48835  gpg5nbgrvtx13starlem1  48836  gpg5nbgrvtx13starlem3  48838  gpg3kgrtriex  48854  inlinecirc02plem  49566  oppcthinendcALT  50219