Theorem neeq2 2988

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  psseq2  4050  prproe  4865  fprg  7109  f1dom3el3dif  7226  f1ounsn  7229  f1prex  7241  resf1extb  7890  xpord2lem  8098  xpord3lem  8105  dfac5  10058  kmlem4  10083  kmlem14  10093  1re  11150  hashge2el2difr  14422  hashdmpropge2  14424  dvdsle  16256  sgrp2rid2ex  18830  isirred  20304  isnzr2  20403  dmatelnd  22359  mdetdiaglem  22461  mdetunilem1  22475  mdetunilem2  22476  maducoeval2  22503  hausnei  23191  regr1lem2  23603  xrhmeo  24820  axtg5seg  28368  axtgupdim2  28374  axtgeucl  28375  ishlg  28505  tglnpt2  28544  axlowdim1  28862  umgrvad2edg  29116  2pthdlem1  29833  3pthdlem1  30066  upgr3v3e3cycl  30082  upgr4cycl4dv4e  30087  eupth2lem3lem4  30133  3cyclfrgrrn1  30187  4cycl2vnunb  30192  numclwwlkovh  30275  numclwwlkovq  30276  numclwwlk2lem1  30278  numclwlk2lem2f  30279  superpos  32256  constrconj  33708  constrcccllem  33717  constrcbvlem  33718  signswch  34525  axtgupdim2ALTV  34632  dfrdg4  35912  fvray  36102  linedegen  36104  fvline  36105  linethru  36114  hilbert1.1  36115  knoppndvlem21  36493  poimirlem1  37588  hlsuprexch  39348  3dim1lem5  39433  llni2  39479  lplni2  39504  2llnjN  39534  lvoli2  39548  2lplnj  39587  islinei  39707  cdleme40n  40435  cdlemg33b  40674  ax6e2ndeq  44522  ax6e2ndeqVD  44871  ax6e2ndeqALT  44893  permac8prim  44977  refsum2cnlem1  45004  stoweidlem43  46014  nnfoctbdjlem  46426  elprneb  47003  ichnreuop  47446  usgrgrtrirex  47922  gpg5nbgrvtx03starlem1  48032  gpg5nbgrvtx03starlem3  48034  gpg5nbgrvtx13starlem1  48035  gpg5nbgrvtx13starlem3  48037  gpg3kgrtriex  48053  inlinecirc02plem  48748  oppcthinendcALT  49403