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

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  |-  ( 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 2654 . 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 1395    =/= wne 2652
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
This theorem is referenced by:  necon3bi  2686  necon2ai  2692  necon3i  2697  ne0i  3799  otsndisj  4761  sdomdif  7684  2pwne  7692  mapdom2  7707  canthp1lem2  9048  wrdlen2i  12896  isprm2  14237  isprm5  14265  sgrp2nmndlem5  16174  maducoeval2  19269  alexsub  20671  ioorf  22108  dvtaylp  22891  isosctrlem1  23278  isosctrlem2  23279  chordthmlem  23289  efrlim  23425  lgsfcl2  23703  lgscllem  23704  lgsval2lem  23707  dchrisumn0  23832  tgbtwnne  24007  tgbtwndiff  24023  tgbtwnconn1lem3  24087  legov3  24110  legso  24111  ncolne1  24131  tglineneq  24150  tglowdim2ln  24158  miriso  24176  mirhl  24185  mirbtwnhl  24186  symquadlem  24192  krippenlem  24193  midexlem  24195  ragflat3  24209  ragperp  24220  footex  24221  colperpexlem2  24231  colperpexlem3  24232  mideulem2  24234  lmieu  24276  lmicom  24280  axlowdim1  24389  eupath  25108  nmcfnlbi  27098  strlem1  27296  divnumden2  27769  2sqn0  27794  2sqmod  27796  xrge0neqmnf  27839  xrge0npcan  27844  ornglmullt  27958  orngrmullt  27959  xrge0iifhom  28080  qqhf  28128  qqhre  28159  logccne0  28173  esumrnmpt2  28240  carsgclctunlem2  28461  ballotlemi1  28638  ballotlemii  28639  ballotlemfrcn0  28665  plymulx0  28701  signswn0  28714  signswch  28715  signstfvneq0  28726  pconcon  28873  nodenselem3  29660  maxidln0  30647  pellexlem6  30974  neqne  31637  n0p  31640  dstregt0  31666  flltnz  31701  upbdrech2  31711  fmul01lt1lem1  31781  limcperiod  31837  sinaover2ne0  31871  dvmptdiv  31917  fperdvper  31918  dvdivbd  31923  itgioocnicc  31979  stirlinglem5  32063  dirker2re  32077  dirkerdenne0  32078  dirkerper  32081  dirkertrigeqlem3  32085  dirkertrigeq  32086  dirkercncflem1  32088  dirkercncflem2  32089  dirkercncflem4  32091  fourierdlem24  32116  fourierdlem25  32117  fourierdlem40  32132  fourierdlem41  32133  fourierdlem42  32134  fourierdlem44  32136  fourierdlem48  32140  fourierdlem49  32141  fourierdlem57  32149  fourierdlem58  32150  fourierdlem59  32151  fourierdlem66  32158  fourierdlem68  32160  fourierdlem74  32166  fourierdlem75  32167  fourierdlem78  32170  fourierdlem80  32172  fourierdlem81  32173  fourierdlem109  32201  elaa2lem  32219  elaa2  32220  etransclem9  32229  etransclem35  32255  etransclem38  32258  sigardiv  32281  sigarcol  32284  sharhght  32285  hdmapip0  37788
  Copyright terms: Public domain W3C validator