Theorem neeq2 2708

Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.)

Assertion

Ref	Expression
neeq2	|- ( A = B -> ( C =/= A <-> C =/= B ) )

Proof of Theorem neeq2

Step	Hyp	Ref	Expression
1		id 23	. 2 |- ( A = B -> A = B )
2	1	neeq2d 2703	1 |- ( A = B -> ( C =/= A <-> C =/= B ) )

Syntax hints:   -> wi 4   <-> wb 188   = wceq 1438   =/= wne 2619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-cleq 2415  df-ne 2621

This theorem is referenced by:  neeq2iOLD  2713  neeq2dOLD  2717  psseq2  3554  fprg  6086  f1dom3el3dif  6182  f1prex  6195  dfac5  8561  kmlem4  8585  kmlem14  8595  1re  9644  hashge2el2difr  12636  dvdsle  14343  sgrp2rid2ex  16654  isirred  17920  isnzr2  18480  dmatelnd  19513  mdetdiaglem  19615  mdetunilem1  19629  mdetunilem2  19630  maducoeval2  19657  hausnei  20336  regr1lem2  20747  xrhmeo  21966  axtg5seg  24505  axtgupdim2  24511  axtgeucl  24512  ishlg  24639  tglnpt2  24678  axlowdim1  24981  2pthoncl  25325  clwlknclwlkdifs  25680  3cyclfrgrarn1  25732  4cycl2vnunb  25737  numclwwlk2lem1  25822  numclwlk2lem2f  25823  superpos  27999  signswch  29452  axtgupdim2OLD  29487  dfrdg4  30717  fvray  30907  linedegen  30909  fvline  30910  linethru  30919  hilbert1.1  30920  poimirlem1  31861  hlsuprexch  32871  3dim1lem5  32956  llni2  33002  lplni2  33027  2llnjN  33057  lvoli2  33071  2lplnj  33110  islinei  33230  cdleme40n  33960  cdlemg33b  34199  ax6e2ndeq  36790  ax6e2ndeqVD  37173  ax6e2ndeqALT  37195  refsum2cnlem1  37225  stoweidlem43  37730  nnfoctbdjlem  38078  elprneb  38430  struct1vtxvallem  38795  usgvad2edg  39027