Theorem neeq2 2994

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539   ≠ wne 2931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726  df-ne 2932

This theorem is referenced by:  psseq2  4071  prproe  4885  fprg  7155  f1dom3el3dif  7271  f1ounsn  7274  f1prex  7286  resf1extb  7938  xpord2lem  8149  xpord3lem  8156  dfac5  10151  kmlem4  10176  kmlem14  10186  1re  11243  hashge2el2difr  14503  hashdmpropge2  14505  dvdsle  16330  sgrp2rid2ex  18910  isirred  20388  isnzr2  20487  dmatelnd  22451  mdetdiaglem  22553  mdetunilem1  22567  mdetunilem2  22568  maducoeval2  22595  hausnei  23283  regr1lem2  23695  xrhmeo  24914  axtg5seg  28410  axtgupdim2  28416  axtgeucl  28417  ishlg  28547  tglnpt2  28586  axlowdim1  28905  umgrvad2edg  29159  2pthdlem1  29879  3pthdlem1  30112  upgr3v3e3cycl  30128  upgr4cycl4dv4e  30133  eupth2lem3lem4  30179  3cyclfrgrrn1  30233  4cycl2vnunb  30238  numclwwlkovh  30321  numclwwlkovq  30322  numclwwlk2lem1  30324  numclwlk2lem2f  30325  superpos  32302  constrconj  33730  constrcccllem  33739  constrcbvlem  33740  signswch  34551  axtgupdim2ALTV  34658  dfrdg4  35927  fvray  36117  linedegen  36119  fvline  36120  linethru  36129  hilbert1.1  36130  knoppndvlem21  36508  poimirlem1  37603  hlsuprexch  39358  3dim1lem5  39443  llni2  39489  lplni2  39514  2llnjN  39544  lvoli2  39558  2lplnj  39597  islinei  39717  cdleme40n  40445  cdlemg33b  40684  ax6e2ndeq  44551  ax6e2ndeqVD  44901  ax6e2ndeqALT  44923  refsum2cnlem1  45014  stoweidlem43  46030  nnfoctbdjlem  46442  elprneb  47014  ichnreuop  47432  usgrgrtrirex  47890  gpg5nbgrvtx03starlem1  47997  gpg5nbgrvtx03starlem3  47999  gpg5nbgrvtx13starlem1  48000  gpg5nbgrvtx13starlem3  48002  gpg3kgrtriex  48018  inlinecirc02plem  48680  oppcthinendcALT  49142