Theorem neeq2 2996

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ≠ wne 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  psseq2  4032  prproe  4849  fprg  7102  f1dom3el3dif  7217  f1ounsn  7220  f1prex  7232  resf1extb  7878  xpord2lem  8085  xpord3lem  8092  dfac5  10042  kmlem4  10067  kmlem14  10077  1re  11135  hashge2el2difr  14434  hashdmpropge2  14436  dvdsle  16270  sgrp2rid2ex  18889  isirred  20390  isnzr2  20486  dmatelnd  22471  mdetdiaglem  22573  mdetunilem1  22587  mdetunilem2  22588  maducoeval2  22615  hausnei  23303  regr1lem2  23715  xrhmeo  24923  axtg5seg  28547  axtgupdim2  28553  axtgeucl  28554  ishlg  28684  tglnpt2  28723  axlowdim1  29042  umgrvad2edg  29296  2pthdlem1  30013  3pthdlem1  30249  upgr3v3e3cycl  30265  upgr4cycl4dv4e  30270  eupth2lem3lem4  30316  3cyclfrgrrn1  30370  4cycl2vnunb  30375  numclwwlkovh  30458  numclwwlkovq  30459  numclwwlk2lem1  30461  numclwlk2lem2f  30462  superpos  32440  constrconj  33905  constrcccllem  33914  constrcbvlem  33915  signswch  34721  axtgupdim2ALTV  34828  dfrdg4  36149  fvray  36339  linedegen  36341  fvline  36342  linethru  36351  hilbert1.1  36352  knoppndvlem21  36808  poimirlem1  37956  hlsuprexch  39841  3dim1lem5  39926  llni2  39972  lplni2  39997  2llnjN  40027  lvoli2  40041  2lplnj  40080  islinei  40200  cdleme40n  40928  cdlemg33b  41167  ax6e2ndeq  45004  ax6e2ndeqVD  45353  ax6e2ndeqALT  45375  permac8prim  45459  refsum2cnlem1  45486  stoweidlem43  46489  nnfoctbdjlem  46901  elprneb  47489  ichnreuop  47944  usgrgrtrirex  48438  gpg5nbgrvtx03starlem1  48556  gpg5nbgrvtx03starlem3  48558  gpg5nbgrvtx13starlem1  48559  gpg5nbgrvtx13starlem3  48561  gpg3kgrtriex  48577  inlinecirc02plem  49274  oppcthinendcALT  49928