Theorem neeq2 2698

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 22	. 2 |- ( A = B -> A = B )
2	1	neeq2d 2695	1 |- ( A = B -> ( C =/= A <-> C =/= B ) )

Syntax hints:   -> wi 4   <-> wb 189   = wceq 1454   =/= wne 2632

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

This theorem depends on definitions:  df-bi 190  df-cleq 2454  df-ne 2634

This theorem is referenced by:  psseq2  3532  fprg  6096  f1dom3el3dif  6193  f1prex  6206  dfac5  8584  kmlem4  8608  kmlem14  8618  1re  9667  hashge2el2difr  12670  dvdsle  14398  sgrp2rid2ex  16709  isirred  17975  isnzr2  18535  dmatelnd  19569  mdetdiaglem  19671  mdetunilem1  19685  mdetunilem2  19686  maducoeval2  19713  hausnei  20392  regr1lem2  20803  xrhmeo  22022  axtg5seg  24561  axtgupdim2  24567  axtgeucl  24568  ishlg  24695  tglnpt2  24734  axlowdim1  25037  2pthoncl  25381  clwlknclwlkdifs  25736  3cyclfrgrarn1  25788  4cycl2vnunb  25793  numclwwlk2lem1  25878  numclwlk2lem2f  25879  superpos  28055  signswch  29498  axtgupdim2OLD  29533  dfrdg4  30766  fvray  30956  linedegen  30958  fvline  30959  linethru  30968  hilbert1.1  30969  poimirlem1  31985  hlsuprexch  32990  3dim1lem5  33075  llni2  33121  lplni2  33146  2llnjN  33176  lvoli2  33190  2lplnj  33229  islinei  33349  cdleme40n  34079  cdlemg33b  34318  ax6e2ndeq  36969  ax6e2ndeqVD  37345  ax6e2ndeqALT  37367  refsum2cnlem1  37397  stoweidlem43  37941  nnfoctbdjlem  38330  elprneb  38749  structgrssvtxlem  39170  2pthdlem1  39878  3pthdlem1  39904  upgr3v3e3cycl  39920  upgr4cycl4dv4e  39925  usgvad2edg  39995