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

Theorem neqned 2642
Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2640. One-way deduction form of df-ne 2635. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2662. (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 2635 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2sylibr 217 1  |-  ( ph  ->  A  =/=  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1455    =/= wne 2633
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 190  df-ne 2635
This theorem is referenced by:  neqne  2643  necon3bi  2662  necon2ai  2665  necon3i  2668  ne0i  3749  otsndisj  4723  sdomdif  7751  2pwne  7759  mapdom2  7774  canthp1lem2  9109  xrge0neqmnf  11771  wrdlen2i  13073  isprm2  14687  isprm5  14706  sgrp2nmndlem5  16718  maducoeval2  19720  alexsub  21115  ioorf  22581  ioorfOLD  22586  dvtaylp  23381  logccne0  23584  isosctrlem1  23803  isosctrlem2  23804  chordthmlem  23814  efrlim  23951  lgsfcl2  24286  lgscllem  24287  lgsval2lem  24290  dchrisumn0  24415  tgbtwnne  24590  tgbtwndiff  24606  tgbtwnconn1lem3  24675  legov3  24699  legso  24700  ncolne1  24726  tglineneq  24745  tglowdim2ln  24752  mirne  24768  miriso  24771  mirhl  24780  mirbtwnhl  24781  symquadlem  24790  krippenlem  24791  midexlem  24793  ragflat3  24807  ragperp  24818  footex  24819  colperpexlem2  24829  colperpexlem3  24830  mideulem2  24832  oppne3  24841  outpasch  24853  hlpasch  24854  lmieu  24882  lmicom  24886  axlowdim1  25045  eupath  25765  nmcfnlbi  27761  strlem1  27959  divnumden2  28433  2sqn0  28459  2sqmod  28461  xrge0npcan  28508  ornglmullt  28621  orngrmullt  28622  xrge0iifhom  28794  qqhf  28841  qqhre  28875  esumrnmpt2  28940  carsgclctunlem2  29201  ballotlemi1  29385  ballotlemii  29386  ballotlemfrcn0  29412  ballotlemi1OLD  29423  ballotlemiiOLD  29424  ballotlemfrcn0OLD  29450  plymulx0  29486  signswn0  29499  signswch  29500  signstfvneq0  29511  pconcon  30004  noseponlem  30605  nodenselem3  30622  sucneqond  31814  finxpreclem2  31828  finxp1o  31830  maxidln0  32324  hdmapip0  35532  pellexlem6  35724  n0p  37415  nelpr2  37479  nelpr1  37480  disjrnmpt2  37517  dstregt0  37566  flltnz  37591  upbdrech2  37601  xrlexaddrp  37650  infleinflem2  37670  fmul01lt1lem1  37748  limcperiod  37794  sinaover2ne0  37829  dvmptdiv  37875  fperdvper  37876  dvdivbd  37881  itgioocnicc  37940  stirlinglem5  38041  dirker2re  38055  dirkerdenne0  38056  dirkerper  38059  dirkertrigeqlem3  38063  dirkertrigeq  38064  dirkercncflem1  38066  dirkercncflem2  38067  dirkercncflem4  38069  fourierdlem24  38094  fourierdlem25  38095  fourierdlem40  38111  fourierdlem41  38112  fourierdlem42  38113  fourierdlem42OLD  38114  fourierdlem44  38116  fourierdlem48  38119  fourierdlem49  38120  fourierdlem57  38128  fourierdlem58  38129  fourierdlem59  38130  fourierdlem66  38137  fourierdlem68  38139  fourierdlem74  38145  fourierdlem75  38146  fourierdlem78  38149  fourierdlem80  38151  fourierdlem81  38152  fourierdlem109  38180  elaa2lem  38198  elaa2lemOLD  38199  etransclem9  38209  etransclem35  38235  etransclem38  38238  sge0tsms  38325  sge0cl  38326  sge0fodjrnlem  38361  meadjun  38405  meadjiunlem  38408  hoicvr  38477  hoidmvlelem2  38525  hoiqssbllem3  38553  sigardiv  38605  sigarcol  38608  sharhght  38609  nbgrssovtx  39578  difmodm1lt  40694
  Copyright terms: Public domain W3C validator