Theorem neqned 2660

Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2659. One-way deduction form of df-ne 2654. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2686. (Revised by Wolf Lammen, 22-Nov-2019.)

Hypothesis

Ref	Expression
neqned.1

Assertion

Ref	Expression
neqned

Proof of Theorem neqned

Step	Hyp	Ref	Expression
1		neqned.1	. 2
2		df-ne 2654	. 2
3	1, 2	sylibr 212	1

Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  =/=wne 2652

This theorem is referenced by:  necon3bi  2686  necon2ai  2692  necon3i  2697  ne0i  3790  otsndisj  4757  sdomdif  7685  2pwne  7693  mapdom2  7708  canthp1lem2  9052  wrdlen2i  12884  isprm2  14225  isprm5  14253  sgrp2nmndlem5  16047  maducoeval2  19142  alexsub  20545  ioorf  21982  dvtaylp  22765  isosctrlem1  23152  isosctrlem2  23153  chordthmlem  23163  efrlim  23299  lgsfcl2  23577  lgscllem  23578  lgsval2lem  23581  dchrisumn0  23706  tgbtwnne  23881  tgbtwndiff  23897  tgbtwnconn1lem3  23961  legov3  23984  legso  23985  ncolne1  24005  tglineneq  24024  tglowdim2ln  24032  miriso  24050  mirhl  24059  mirbtwnhl  24060  symquadlem  24066  krippenlem  24067  midexlem  24069  ragflat3  24083  ragperp  24094  footex  24095  colperpexlem2  24105  colperpexlem3  24106  mideulem2  24108  lmieu  24150  lmicom  24154  axlowdim1  24262  eupath  24981  nmcfnlbi  26971  strlem1  27169  divnumden2  27609  2sqn0  27634  2sqmod  27636  xrge0neqmnf  27679  xrge0npcan  27684  ornglmullt  27797  orngrmullt  27798  xrge0iifhom  27919  qqhf  27967  qqhre  27998  logccne0  28012  ballotlemi1  28441  ballotlemii  28442  ballotlemfrcn0  28468  plymulx0  28504  signswn0  28517  signswch  28518  signstfvneq0  28529  pconcon  28676  nodenselem3  29443  maxidln0  30442  pellexlem6  30770  neqne  31434  n0p  31437  dstregt0  31463  flltnz  31498  upbdrech2  31508  fmul01lt1lem1  31578  limcperiod  31634  sinaover2ne0  31668  dvmptdiv  31714  fperdvper  31715  dvdivbd  31720  itgioocnicc  31776  stirlinglem5  31860  dirker2re  31874  dirkerdenne0  31875  dirkerper  31878  dirkertrigeqlem3  31882  dirkertrigeq  31883  dirkercncflem1  31885  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem24  31913  fourierdlem25  31914  fourierdlem40  31929  fourierdlem41  31930  fourierdlem42  31931  fourierdlem44  31933  fourierdlem48  31937  fourierdlem49  31938  fourierdlem57  31946  fourierdlem58  31947  fourierdlem59  31948  fourierdlem66  31955  fourierdlem68  31957  fourierdlem74  31963  fourierdlem75  31964  fourierdlem78  31967  fourierdlem80  31969  fourierdlem81  31970  fourierdlem109  31998  elaa2lem  32016  elaa2  32017  etransclem9  32026  etransclem35  32052  etransclem38  32055  sigardiv  32078  sigarcol  32081  sharhght  32082  hdmapip0  37645

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

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