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

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

Proof of Theorem nne
StepHypRef Expression
1 df-ne 2944 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
21con2bii 346 . 2 (𝐴 = 𝐵 ↔ ¬ 𝐴𝐵)
32bicomi 214 1 𝐴𝐵𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196   = wceq 1631  wne 2943
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 2944
This theorem is referenced by:  neirr  2952  necon3bd  2957  necon1d  2965  necon4d  2967  necon3ai  2968  necon4bid  2988  necon1bbii  2992  pm2.61ine  3026  pm2.61dne  3029  ne3anior  3036  sbcne12  4130  raldifsnb  4462  tpprceq3  4470  tppreqb  4471  prneimg  4519  prnebg  4520  xpeq0  5695  xpcan  5711  xpcan2  5712  fndmdifeq0  6466  ftpg  6566  fnnfpeq0  6588  suppimacnv  7457  fnsuppres  7474  ixp0  8095  isfin5-2  9415  zornn0g  9529  nn0n0n1ge2b  11561  fsuppmapnn0fiub0  13000  fsuppmapnn0ub  13002  mptnn0fsupp  13004  mptnn0fsuppr  13006  discr  13208  hashgt12el  13412  hashgt12el2  13413  hashtpg  13469  fprodle  14933  alzdvds  15251  algcvgblem  15498  lcmfunsnlem2lem2  15560  lssne0  19161  dsmm0cl  20301  pmatcollpw2lem  20802  elcls  21098  cmpfi  21432  bwth  21434  1stccnp  21486  dissnlocfin  21553  trfil3  21912  isufil2  21932  bcth3  23347  rrxmvallem  23406  mdegleb  24044  tglowdim1i  25617  tglineintmo  25758  lmieu  25897  uhgrvd00  26665  wlkon2n0  26797  wwlks  26963  rusgrnumwwlks  27123  clwwlkneq0  27183  1to2vfriswmgr  27461  numclwwlk3lemOLD  27580  numclwwlk3lem2  27583  frgrregord013  27594  nmlno0lem  27988  lnon0  27993  nmlnop0iALT  29194  atom1d  29552  uniinn0  29704  funcnv5mpt  29809  xaddeq0  29858  bnj521  31143  bnj1533  31260  bnj1541  31264  bnj1279  31424  bnj1280  31426  bnj1311  31430  nepss  31937  poimirlem31  33773  poimirlem32  33774  itg2addnclem2  33794  ftc1anc  33825  n0elqs  34441  lfl1  34879  lkreqN  34979  pmap0  35573  paddasslem17  35644  ltrnnid  35944  ntrneikb  38918  fzdifsuc2  40041  limclr  40405  fourierdlem42  40883  fourierdlem76  40916  sge0cl  41115  meadjiunlem  41199  oddprmne2  42152  mndpsuppss  42680  islininds2  42801
  Copyright terms: Public domain W3C validator