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

Theorem neqned 2623
Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2621. One-way deduction form of df-ne 2616. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2649. (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 2616 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2sylibr 215 1  |-  ( ph  ->  A  =/=  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1437    =/= wne 2614
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 188  df-ne 2616
This theorem is referenced by:  necon3bi  2649  necon2ai  2655  necon3i  2660  ne0i  3767  otsndisj  4725  sdomdif  7729  2pwne  7737  mapdom2  7752  canthp1lem2  9085  xrge0neqmnf  11744  wrdlen2i  13021  isprm2  14631  isprm5  14650  sgrp2nmndlem5  16662  maducoeval2  19663  alexsub  21058  ioorf  22523  ioorfOLD  22528  dvtaylp  23323  logccne0  23526  isosctrlem1  23745  isosctrlem2  23746  chordthmlem  23756  efrlim  23893  lgsfcl2  24228  lgscllem  24229  lgsval2lem  24232  dchrisumn0  24357  tgbtwnne  24532  tgbtwndiff  24548  tgbtwnconn1lem3  24617  legov3  24641  legso  24642  ncolne1  24668  tglineneq  24687  tglowdim2ln  24694  mirne  24710  miriso  24713  mirhl  24722  mirbtwnhl  24723  symquadlem  24732  krippenlem  24733  midexlem  24735  ragflat3  24749  ragperp  24760  footex  24761  colperpexlem2  24771  colperpexlem3  24772  mideulem2  24774  oppne3  24783  outpasch  24795  hlpasch  24796  lmieu  24824  lmicom  24828  axlowdim1  24987  eupath  25707  nmcfnlbi  27703  strlem1  27901  divnumden2  28388  2sqn0  28414  2sqmod  28416  xrge0npcan  28464  ornglmullt  28578  orngrmullt  28579  xrge0iifhom  28751  qqhf  28798  qqhre  28832  esumrnmpt2  28897  carsgclctunlem2  29159  ballotlemi1  29343  ballotlemii  29344  ballotlemfrcn0  29370  ballotlemi1OLD  29381  ballotlemiiOLD  29382  ballotlemfrcn0OLD  29408  plymulx0  29444  signswn0  29457  signswch  29458  signstfvneq0  29469  pconcon  29962  nodenselem3  30577  sucneqond  31732  finxpreclem2  31746  finxp1o  31748  maxidln0  32242  hdmapip0  35455  pellexlem6  35648  neqne  37347  n0p  37349  disjrnmpt2  37424  dstregt0  37445  flltnz  37470  upbdrech2  37480  xrlexaddrp  37529  fmul01lt1lem1  37602  limcperiod  37648  sinaover2ne0  37683  dvmptdiv  37729  fperdvper  37730  dvdivbd  37735  itgioocnicc  37794  stirlinglem5  37880  dirker2re  37894  dirkerdenne0  37895  dirkerper  37898  dirkertrigeqlem3  37902  dirkertrigeq  37903  dirkercncflem1  37905  dirkercncflem2  37906  dirkercncflem4  37908  fourierdlem24  37933  fourierdlem25  37934  fourierdlem40  37950  fourierdlem41  37951  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem44  37955  fourierdlem48  37958  fourierdlem49  37959  fourierdlem57  37967  fourierdlem58  37968  fourierdlem59  37969  fourierdlem66  37976  fourierdlem68  37978  fourierdlem74  37984  fourierdlem75  37985  fourierdlem78  37988  fourierdlem80  37990  fourierdlem81  37991  fourierdlem109  38019  elaa2lem  38037  elaa2lemOLD  38038  etransclem9  38048  etransclem35  38074  etransclem38  38077  sge0tsms  38130  sge0cl  38131  sge0fodjrnlem  38166  meadjun  38208  meadjiunlem  38211  hoicvr  38274  hoidmvlelem2  38322  sigardiv  38341  sigarcol  38344  sharhght  38345  nbgrssovtx  39197  difmodm1lt  39947
  Copyright terms: Public domain W3C validator