Theorem neeq2 2857

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 2854	1 |- ( A = B -> ( C =/= A <-> C =/= B ) )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   =/= wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-ne 2795

This theorem is referenced by:  psseq2  3695  prproe  4434  fprg  6422  f1dom3el3dif  6526  f1prex  6539  dfac5  8951  kmlem4  8975  kmlem14  8985  1re  10039  hashge2el2difr  13263  hashdmpropge2  13265  dvdsle  15032  sgrp2rid2ex  17414  isirred  18699  isnzr2  19263  dmatelnd  20302  mdetdiaglem  20404  mdetunilem1  20418  mdetunilem2  20419  maducoeval2  20446  hausnei  21132  regr1lem2  21543  xrhmeo  22745  axtg5seg  25364  axtgupdim2  25370  axtgeucl  25371  ishlg  25497  tglnpt2  25536  axlowdim1  25839  structgrssvtxlemOLD  25915  umgrvad2edg  26105  2pthdlem1  26826  clwwlknclwwlkdifs  26873  3pthdlem1  27024  upgr3v3e3cycl  27040  upgr4cycl4dv4e  27045  eupth2lem3lem4  27091  3cyclfrgrrn1  27149  4cycl2vnunb  27154  numclwwlkovq  27232  numclwwlk2lem1  27235  numclwlk2lem2f  27236  superpos  29213  signswch  30638  axtgupdim2OLD  30746  dfrdg4  32058  fvray  32248  linedegen  32250  fvline  32251  linethru  32260  hilbert1.1  32261  knoppndvlem21  32523  poimirlem1  33410  hlsuprexch  34667  3dim1lem5  34752  llni2  34798  lplni2  34823  2llnjN  34853  lvoli2  34867  2lplnj  34906  islinei  35026  cdleme40n  35756  cdlemg33b  35995  ax6e2ndeq  38775  ax6e2ndeqVD  39145  ax6e2ndeqALT  39167  refsum2cnlem1  39196  stoweidlem43  40260  nnfoctbdjlem  40672  elprneb  41296