Theorem neeq2 2688

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

Syntax hints:   -> wi 4   <-> wb 186   = wceq 1407   =/= wne 2600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-ext 2382

This theorem depends on definitions:  df-bi 187  df-cleq 2396  df-ne 2602

This theorem is referenced by:  neeq2iOLD  2693  neeq2dOLD  2697  psseq2  3533  fprg  6062  f1dom3el3dif  6159  f1prex  6172  dfac5  8543  kmlem4  8567  kmlem14  8577  1re  9627  dvdsle  14242  sgrp2rid2ex  16371  isirred  17670  isnzr2  18233  dmatelnd  19292  mdetdiaglem  19394  mdetunilem1  19408  mdetunilem2  19409  maducoeval2  19436  hausnei  20124  regr1lem2  20535  xrhmeo  21740  axtg5seg  24243  axtgupdim2  24249  axtgeucl  24250  ishlg  24372  tglnpt2  24410  acopy  24590  axlowdim1  24691  2pthoncl  25034  clwlknclwlkdifs  25389  3cyclfrgrarn1  25441  4cycl2vnunb  25446  numclwwlk2lem1  25531  numclwlk2lem2f  25532  superpos  27699  signswch  29037  axtgupdim2OLD  29072  dfrdg4  30302  fvray  30492  linedegen  30494  fvline  30495  linethru  30504  hilbert1.1  30505  hlsuprexch  32411  3dim1lem5  32496  llni2  32542  lplni2  32567  2llnjN  32597  lvoli2  32611  2lplnj  32650  islinei  32770  cdleme40n  33500  cdlemg33b  33739  ax6e2ndeq  36369  ax6e2ndeqVD  36753  ax6e2ndeqALT  36775  refsum2cnlem1  36805  stoweidlem43  37206  elprneb  37676  usgvad2edg  38053