Theorem neeq2 2991

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

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

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 2121  ax-ext 2703

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

This theorem is referenced by:  psseq2  4036  prproe  4852  fprg  7083  f1dom3el3dif  7198  f1ounsn  7201  f1prex  7213  resf1extb  7859  xpord2lem  8067  xpord3lem  8074  dfac5  10015  kmlem4  10040  kmlem14  10050  1re  11107  hashge2el2difr  14383  hashdmpropge2  14385  dvdsle  16216  sgrp2rid2ex  18830  isirred  20332  isnzr2  20428  dmatelnd  22406  mdetdiaglem  22508  mdetunilem1  22522  mdetunilem2  22523  maducoeval2  22550  hausnei  23238  regr1lem2  23650  xrhmeo  24866  axtg5seg  28438  axtgupdim2  28444  axtgeucl  28445  ishlg  28575  tglnpt2  28614  axlowdim1  28932  umgrvad2edg  29186  2pthdlem1  29903  3pthdlem1  30136  upgr3v3e3cycl  30152  upgr4cycl4dv4e  30157  eupth2lem3lem4  30203  3cyclfrgrrn1  30257  4cycl2vnunb  30262  numclwwlkovh  30345  numclwwlkovq  30346  numclwwlk2lem1  30348  numclwlk2lem2f  30349  superpos  32326  constrconj  33750  constrcccllem  33759  constrcbvlem  33760  signswch  34566  axtgupdim2ALTV  34673  dfrdg4  35985  fvray  36175  linedegen  36177  fvline  36178  linethru  36187  hilbert1.1  36188  knoppndvlem21  36566  poimirlem1  37661  hlsuprexch  39420  3dim1lem5  39505  llni2  39551  lplni2  39576  2llnjN  39606  lvoli2  39620  2lplnj  39659  islinei  39779  cdleme40n  40507  cdlemg33b  40746  ax6e2ndeq  44592  ax6e2ndeqVD  44941  ax6e2ndeqALT  44963  permac8prim  45047  refsum2cnlem1  45074  stoweidlem43  46081  nnfoctbdjlem  46493  elprneb  47060  ichnreuop  47503  usgrgrtrirex  47981  gpg5nbgrvtx03starlem1  48099  gpg5nbgrvtx03starlem3  48101  gpg5nbgrvtx13starlem1  48102  gpg5nbgrvtx13starlem3  48104  gpg3kgrtriex  48120  inlinecirc02plem  48818  oppcthinendcALT  49473