Theorem neeq2 2740

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

Assertion

Ref	Expression
neeq2

Proof of Theorem neeq2

Step	Hyp	Ref	Expression
1		id 22	. 2
2	1	neeq2d 2735	1

Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  =/=wne 2652

This theorem is referenced by:  neeq2iOLD  2745  neeq2dOLD  2749  psseq2  3591  fprg  6080  f1dom3el3dif  6176  dfac5  8530  kmlem4  8554  kmlem14  8564  1re  9616  dvdsle  14031  sgrp2rid2ex  16045  isirred  17348  isnzr2  17911  dmatelnd  18998  mdetdiaglem  19100  mdetunilem1  19114  mdetunilem2  19115  maducoeval2  19142  hausnei  19829  regr1lem2  20241  xrhmeo  21446  axtg5seg  23862  axtgupdim2  23869  axtgeucl  23870  ishlg  23986  tglnpt2  24021  axlowdim1  24262  2pthoncl  24605  clwlknclwlkdifs  24960  3cyclfrgrarn1  25012  4cycl2vnunb  25017  numclwwlk2lem1  25102  numclwlk2lem2f  25103  superpos  27273  signswch  28518  dfrdg4  29600  fvray  29791  linedegen  29793  fvline  29794  linethru  29803  hilbert1.1  29804  refsum2cnlem1  31412  stoweidlem43  31825  usgvad2edg  32411  ax6e2ndeq  33332  ax6e2ndeqVD  33709  ax6e2ndeqALT  33731  hlsuprexch  35105  3dim1lem5  35190  llni2  35236  lplni2  35261  2llnjN  35291  lvoli2  35305  2lplnj  35344  islinei  35464  cdleme40n  36194  cdlemg33b  36433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-cleq 2449  df-ne 2654