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

Theorem neqned 2634
Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2632. One-way deduction form of df-ne 2627. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2660. (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 2627 . 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 2625
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 2627
This theorem is referenced by:  necon3bi  2660  necon2ai  2666  necon3i  2671  ne0i  3773  otsndisj  4726  sdomdif  7726  2pwne  7734  mapdom2  7749  canthp1lem2  9077  wrdlen2i  13000  isprm2  14603  isprm5  14622  sgrp2nmndlem5  16614  maducoeval2  19596  alexsub  20991  ioorf  22402  ioorfOLD  22407  dvtaylp  23190  logccne0  23393  isosctrlem1  23612  isosctrlem2  23613  chordthmlem  23623  efrlim  23760  lgsfcl2  24093  lgscllem  24094  lgsval2lem  24097  dchrisumn0  24222  tgbtwnne  24397  tgbtwndiff  24413  tgbtwnconn1lem3  24479  legov3  24503  legso  24504  ncolne1  24529  tglineneq  24548  tglowdim2ln  24556  miriso  24574  mirhl  24583  mirbtwnhl  24584  symquadlem  24591  krippenlem  24592  midexlem  24594  ragflat3  24608  ragperp  24619  footex  24620  colperpexlem2  24630  colperpexlem3  24631  mideulem2  24633  oppne3  24642  outpasch  24654  lmieu  24682  lmicom  24686  axlowdim1  24835  eupath  25554  nmcfnlbi  27540  strlem1  27738  divnumden2  28219  2sqn0  28245  2sqmod  28247  xrge0neqmnf  28290  xrge0npcan  28295  ornglmullt  28409  orngrmullt  28410  xrge0iifhom  28582  qqhf  28629  qqhre  28663  esumrnmpt2  28728  carsgclctunlem2  28980  ballotlemi1  29161  ballotlemii  29162  ballotlemfrcn0  29188  plymulx0  29224  signswn0  29237  signswch  29238  signstfvneq0  29249  pconcon  29742  nodenselem3  30357  maxidln0  31981  hdmapip0  35194  pellexlem6  35387  neqne  37013  n0p  37015  disjrnmpt2  37085  dstregt0  37099  flltnz  37124  upbdrech2  37134  fmul01lt1lem1  37233  limcperiod  37279  sinaover2ne0  37314  dvmptdiv  37360  fperdvper  37361  dvdivbd  37366  itgioocnicc  37422  stirlinglem5  37508  dirker2re  37522  dirkerdenne0  37523  dirkerper  37526  dirkertrigeqlem3  37530  dirkertrigeq  37531  dirkercncflem1  37533  dirkercncflem2  37534  dirkercncflem4  37536  fourierdlem24  37561  fourierdlem25  37562  fourierdlem40  37577  fourierdlem41  37578  fourierdlem42  37579  fourierdlem44  37581  fourierdlem48  37585  fourierdlem49  37586  fourierdlem57  37594  fourierdlem58  37595  fourierdlem59  37596  fourierdlem66  37603  fourierdlem68  37605  fourierdlem74  37611  fourierdlem75  37612  fourierdlem78  37615  fourierdlem80  37617  fourierdlem81  37618  fourierdlem109  37646  elaa2lem  37664  elaa2  37665  etransclem9  37674  etransclem35  37700  etransclem38  37703  sge0tsms  37755  sge0cl  37756  sge0fodjrnlem  37791  meadjun  37808  meadjiunlem  37811  sigardiv  37869  sigarcol  37872  sharhght  37873  difmodm1lt  39085
  Copyright terms: Public domain W3C validator