Theorem neeq2 3010

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ≠ wne 2946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ne 2947

This theorem is referenced by:  psseq2  4114  prproe  4929  fprg  7189  f1dom3el3dif  7306  f1prex  7320  xpord2lem  8183  xpord3lem  8190  dfac5  10198  kmlem4  10223  kmlem14  10233  1re  11290  hashge2el2difr  14530  hashdmpropge2  14532  dvdsle  16358  sgrp2rid2ex  18962  isirred  20445  isnzr2  20544  dmatelnd  22523  mdetdiaglem  22625  mdetunilem1  22639  mdetunilem2  22640  maducoeval2  22667  hausnei  23357  regr1lem2  23769  xrhmeo  24996  axtg5seg  28491  axtgupdim2  28497  axtgeucl  28498  ishlg  28628  tglnpt2  28667  axlowdim1  28992  umgrvad2edg  29248  2pthdlem1  29963  3pthdlem1  30196  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  eupth2lem3lem4  30263  3cyclfrgrrn1  30317  4cycl2vnunb  30322  numclwwlkovh  30405  numclwwlkovq  30406  numclwwlk2lem1  30408  numclwlk2lem2f  30409  superpos  32386  constrconj  33735  signswch  34538  axtgupdim2ALTV  34645  dfrdg4  35915  fvray  36105  linedegen  36107  fvline  36108  linethru  36117  hilbert1.1  36118  knoppndvlem21  36498  poimirlem1  37581  hlsuprexch  39338  3dim1lem5  39423  llni2  39469  lplni2  39494  2llnjN  39524  lvoli2  39538  2lplnj  39577  islinei  39697  cdleme40n  40425  cdlemg33b  40664  ax6e2ndeq  44530  ax6e2ndeqVD  44880  ax6e2ndeqALT  44902  refsum2cnlem1  44937  stoweidlem43  45964  nnfoctbdjlem  46376  elprneb  46944  ichnreuop  47346  usgrgrtrirex  47799  inlinecirc02plem  48520