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

Theorem nne 2994
Description: Negation of inequality. (Contributed by NM, 9-Jun-2006.)
Assertion
Ref Expression
nne 𝐴𝐵𝐴 = 𝐵)

Proof of Theorem nne
StepHypRef Expression
1 df-ne 2991 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
21con2bii 361 . 2 (𝐴 = 𝐵 ↔ ¬ 𝐴𝐵)
32bicomi 227 1 𝐴𝐵𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 209   = wceq 1538  wne 2990
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 210  df-ne 2991
This theorem is referenced by:  neirr  2999  necon3bd  3004  necon1d  3012  necon4d  3014  necon3ai  3015  necon4bid  3035  necon1bbii  3039  pm2.61ine  3073  pm2.61dne  3076  ne3anior  3083  sbcne12  4323  raldifsnb  4692  tpprceq3  4700  tppreqb  4701  prneimg  4748  prnebg  4749  xpeq0  5988  xpcan  6004  xpcan2  6005  fndmdifeq0  6795  ftpg  6899  fnnfpeq0  6921  suppimacnv  7828  fnsuppres  7844  suppcoss  7858  ixp0  8482  isfin5-2  9806  zornn0g  9920  nn0n0n1ge2b  11955  fsuppmapnn0fiub0  13360  fsuppmapnn0ub  13362  mptnn0fsupp  13364  mptnn0fsuppr  13366  discr  13601  hashgt12el  13783  hashgt12el2  13784  hashtpg  13843  fprodle  15346  alzdvds  15666  algcvgblem  15915  lcmfunsnlem2lem2  15977  lssne0  19719  dsmm0cl  20433  pmatcollpw2lem  21386  elcls  21682  cmpfi  22017  bwth  22019  1stccnp  22071  dissnlocfin  22138  trfil3  22497  isufil2  22517  bcth3  23939  rrxmvallem  24012  mdegleb  24669  tglowdim1i  26299  tglineintmo  26440  lmieu  26582  uhgrvd00  27328  wlkon2n0  27460  wwlks  27625  rusgrnumwwlks  27764  clwwlkneq0  27818  1to2vfriswmgr  28068  numclwwlk3lem2  28173  frgrregord013  28184  nmlno0lem  28580  lnon0  28585  nmlnop0iALT  29782  atom1d  30140  uniinn0  30318  nfpconfp  30395  funcnv5mpt  30435  suppiniseg  30450  xaddeq0  30507  pmtrcnel  30787  fedgmullem2  31118  zarcls1  31226  bnj521  32121  bnj1533  32238  bnj1541  32242  bnj1279  32404  bnj1280  32406  bnj1311  32410  spthcycl  32490  nepss  33062  bj-ismooredr2  34526  nlpineqsn  34826  poimirlem31  35087  poimirlem32  35088  itg2addnclem2  35108  ftc1anc  35137  n0elqs  35742  lfl1  36365  lkreqN  36465  pmap0  37060  paddasslem17  37131  ltrnnid  37431  dffltz  39608  ntrneikb  40790  fzdifsuc2  41935  limclr  42290  liminflbuz2  42450  fourierdlem42  42784  fourierdlem76  42817  sge0cl  43013  meadjiunlem  43097  oddprmne2  44226  mndpsuppss  44766  islininds2  44886  line2ylem  45158  line2xlem  45160  itsclc0xyqsol  45175  2itscp  45188
  Copyright terms: Public domain W3C validator