MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  neqned Structured version   Unicode version

Theorem neqned 2670
Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2669. One-way deduction form of df-ne 2664. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2696. (Revised by Wolf Lammen, 22-Nov-2019.)
Hypothesis
Ref Expression
neqned.1  |-  ( ph  ->  -.  A  =  B )
Assertion
Ref Expression
neqned  |-  ( ph  ->  A  =/=  B )

Proof of Theorem neqned
StepHypRef Expression
1 neqned.1 . 2  |-  ( ph  ->  -.  A  =  B )
2 df-ne 2664 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2sylibr 212 1  |-  ( ph  ->  A  =/=  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1379    =/= wne 2662
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 2664
This theorem is referenced by:  necon3bi  2696  necon2ai  2702  necon3i  2707  ne0i  3796  otsndisj  4758  sdomdif  7677  2pwne  7685  mapdom2  7700  canthp1lem2  9043  wrdlen2i  12864  isprm2  14101  isprm5  14129  maducoeval2  19011  alexsub  20413  ioorf  21850  dvtaylp  22632  isosctrlem1  23018  isosctrlem2  23019  chordthmlem  23029  efrlim  23165  lgsfcl2  23443  lgscllem  23444  lgsval2lem  23447  dchrisumn0  23572  tgbtwnne  23747  tgbtwndiff  23763  tgbtwnconn1lem3  23826  legov3  23849  legso  23850  ncolne1  23858  ncolne2  23859  tglineneq  23876  tglowdim2ln  23884  miriso  23902  symquadlem  23914  krippenlem  23915  midexlem  23917  ragflat3  23931  ragperp  23942  footex  23943  colperpexlem2  23950  colperpexlem3  23951  mideulem2  23953  lmieu  23974  lmicom  23978  axlowdim1  24085  eupath  24804  nmcfnlbi  26794  strlem1  26992  divnumden2  27432  2sqn0  27458  2sqmod  27460  xrge0neqmnf  27503  xrge0npcan  27508  ornglmullt  27622  orngrmullt  27623  xrge0iifhom  27744  qqhf  27792  qqhre  27823  logccne0  27837  ballotlemi1  28266  ballotlemii  28267  ballotlemfrcn0  28293  plymulx0  28329  signswn0  28342  signswch  28343  signstfvneq0  28354  pconcon  28501  nodenselem3  29370  maxidln0  30369  pellexlem6  30698  neqne  31339  dstregt0  31363  flltnz  31398  fzisoeu  31400  upbdrech2  31408  limcperiod  31493  sinaover2ne0  31527  cncfiooiccre  31557  dvmptdiv  31570  fperdvper  31571  dvdivbd  31576  itgioocnicc  31618  stirlinglem5  31701  dirker2re  31715  dirkerdenne0  31716  dirkerval2  31717  dirkerper  31719  dirkertrigeqlem3  31723  dirkertrigeq  31724  dirkercncflem1  31726  dirkercncflem2  31727  dirkercncflem4  31729  fourierdlem9  31739  fourierdlem24  31754  fourierdlem25  31755  fourierdlem33  31763  fourierdlem41  31771  fourierdlem42  31772  fourierdlem44  31774  fourierdlem48  31778  fourierdlem49  31779  fourierdlem54  31784  fourierdlem57  31787  fourierdlem58  31788  fourierdlem59  31789  fourierdlem65  31795  fourierdlem66  31796  fourierdlem68  31798  fourierdlem74  31804  fourierdlem75  31805  fourierdlem79  31809  fourierdlem80  31810  fourierdlem81  31811  fourierdlem109  31839  fourierswlem  31854  fouriersw  31855  sigardiv  31868  sigarcol  31871  sharhght  31872  sgrp2nmndlem5ALT  32256  hdmapip0  37116
  Copyright terms: Public domain W3C validator