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

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

Proof of Theorem nne
StepHypRef Expression
1 df-ne 2945 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
21con2bii 358 . 2 (𝐴 = 𝐵 ↔ ¬ 𝐴𝐵)
32bicomi 223 1 𝐴𝐵𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205   = wceq 1542  wne 2944
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 206  df-ne 2945
This theorem is referenced by:  neirr  2953  necon3bd  2958  necon1d  2966  necon4d  2968  necon3aiOLD  2970  necon4bid  2990  necon1bbii  2994  pm2.61ine  3029  ne3anior  3039  sbcne12  4373  raldifsnb  4757  tpprceq3  4765  tppreqb  4766  prneimg  4813  prnebg  4814  xpeq0  6113  xpcan  6129  xpcan2  6130  fndmdifeq0  6995  ftpg  7103  fnnfpeq0  7125  suppimacnv  8106  fnsuppres  8123  suppcoss  8139  ixp0  8870  isfin5-2  10328  zornn0g  10442  nn0n0n1ge2b  12482  fsuppmapnn0fiub0  13899  fsuppmapnn0ub  13901  mptnn0fsupp  13903  mptnn0fsuppr  13905  discr  14144  hashgt12el  14323  hashgt12el2  14324  hashtpg  14385  fprodle  15880  alzdvds  16203  algcvgblem  16454  lcmfunsnlem2lem2  16516  lssne0  20414  dsmm0cl  21149  pmatcollpw2lem  22129  elcls  22427  cmpfi  22762  bwth  22764  1stccnp  22816  dissnlocfin  22883  trfil3  23242  isufil2  23262  bcth3  24698  rrxmvallem  24771  mdegleb  25432  tglowdim1i  27446  tglineintmo  27587  lmieu  27729  uhgrvd00  28485  wlkon2n0  28617  wwlks  28783  rusgrnumwwlks  28922  clwwlkneq0  28976  1to2vfriswmgr  29226  numclwwlk3lem2  29331  frgrregord013  29342  nmlno0lem  29738  lnon0  29743  nmlnop0iALT  30940  atom1d  31298  uniinn0  31472  nfpconfp  31549  funcnv5mpt  31587  suppiniseg  31604  xaddeq0  31661  pmtrcnel  31943  fedgmullem2  32328  zarcls1  32453  bnj1533  33467  bnj1541  33471  bnj1279  33633  bnj1280  33635  bnj1311  33639  spthcycl  33726  nepss  34292  bj-ismooredr2  35584  nlpineqsn  35882  poimirlem31  36112  poimirlem32  36113  itg2addnclem2  36133  ftc1anc  36162  n0elqs  36790  lfl1  37535  lkreqN  37635  pmap0  38231  paddasslem17  38302  ltrnnid  38602  sticksstones1  40557  dffltz  40975  dflim5  41666  ntrneikb  42373  fzdifsuc2  43551  limclr  43903  liminflbuz2  44063  fourierdlem42  44397  fourierdlem76  44430  sge0cl  44629  meadjiunlem  44713  smfpimne2  45088  oddprmne2  45914  mndpsuppss  46454  islininds2  46572  line2ylem  46844  line2xlem  46846  itsclc0xyqsol  46861  2itscp  46874  fdomne0  46923
  Copyright terms: Public domain W3C validator