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

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

Proof of Theorem nne
StepHypRef Expression
1 df-ne 2824 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
21con2bii 346 . 2 (𝐴 = 𝐵 ↔ ¬ 𝐴𝐵)
32bicomi 214 1 𝐴𝐵𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196   = wceq 1523  wne 2823
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 197  df-ne 2824
This theorem is referenced by:  neirr  2832  necon3bd  2837  necon1d  2845  necon4d  2847  necon3ai  2848  necon4bid  2868  necon1bbii  2872  pm2.61ine  2906  pm2.61dne  2909  ne3anior  2916  sbcne12  4019  raldifsnb  4358  tpprceq3  4367  tppreqb  4368  prneimg  4419  prnebg  4420  xpeq0  5589  xpcan  5605  xpcan2  5606  funtpgOLD  5981  fndmdifeq0  6363  ftpg  6463  fnnfpeq0  6485  suppimacnv  7351  fnsuppres  7367  ixp0  7983  isfin5-2  9251  zornn0g  9365  nn0n0n1ge2b  11397  fsuppmapnn0fiub0  12833  fsuppmapnn0ub  12835  mptnn0fsupp  12837  mptnn0fsuppr  12839  discr  13041  hashgt12el  13248  hashgt12el2  13249  hashtpg  13305  fprodle  14771  alzdvds  15089  algcvgblem  15337  lcmfunsnlem2lem2  15399  lssne0  18999  dsmm0cl  20132  pmatcollpw2lem  20630  elcls  20925  cmpfi  21259  bwth  21261  1stccnp  21313  dissnlocfin  21380  trfil3  21739  isufil2  21759  bcth3  23174  rrxmvallem  23233  mdegleb  23869  tglowdim1i  25441  tglineintmo  25582  lmieu  25721  uhgrvd00  26486  wlkon2n0  26618  wwlks  26783  rusgrnumwwlks  26941  clwwlkneq0  26990  1to2vfriswmgr  27259  numclwwlk3lemOLD  27369  numclwwlk3lem  27371  frgrregord013  27382  nmlno0lem  27776  lnon0  27781  nmlnop0iALT  28982  atom1d  29340  uniinn0  29492  funcnv5mpt  29597  xaddeq0  29646  bnj521  30931  bnj1533  31048  bnj1541  31052  bnj1279  31212  bnj1280  31214  bnj1311  31218  nepss  31725  poimirlem31  33570  poimirlem32  33571  itg2addnclem2  33592  ftc1anc  33623  n0elqs  34239  lfl1  34675  lkreqN  34775  pmap0  35369  paddasslem17  35440  ltrnnid  35740  ntrneikb  38709  fzdifsuc2  39838  limclr  40205  fourierdlem42  40684  fourierdlem76  40717  sge0cl  40916  meadjiunlem  41000  oddprmne2  41949  mndpsuppss  42477  islininds2  42598
  Copyright terms: Public domain W3C validator