Theorem neeq2 2750

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1379   =/= wne 2662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-cleq 2459  df-ne 2664

This theorem is referenced by:  neeq2iOLD  2755  neeq2dOLD  2759  psseq2  3592  fprg  6068  f1dom3el3dif  6162  dfac5  8505  kmlem4  8529  kmlem14  8539  1re  9591  dvdsle  13886  isirred  17132  isnzr2  17693  dmatelnd  18765  mdetdiaglem  18867  mdetunilem1  18881  mdetunilem2  18882  maducoeval2  18909  hausnei  19595  regr1lem2  19976  xrhmeo  21181  axtg5seg  23590  axtgupdim2  23597  axtgeucl  23598  tglnpt2  23734  axlowdim1  23938  2pthoncl  24281  clwlknclwlkdifs  24636  3cyclfrgrarn1  24688  4cycl2vnunb  24693  numclwwlk2lem1  24779  numclwlk2lem2f  24780  superpos  26949  signswch  28158  dfrdg4  29177  fvray  29368  linedegen  29370  fvline  29371  linethru  29380  hilbert1.1  29381  refsum2cnlem1  30990  stoweidlem43  31343  usgvad2edg  31880  ax6e2ndeq  32412  ax6e2ndeqVD  32789  ax6e2ndeqALT  32811  hlsuprexch  34177  3dim1lem5  34262  llni2  34308  lplni2  34333  2llnjN  34363  lvoli2  34377  2lplnj  34416  islinei  34536  cdleme40n  35264  cdlemg33b  35503