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

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

Proof of Theorem nne
StepHypRef Expression
1 df-ne 3017 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
21con2bii 359 . 2 (𝐴 = 𝐵 ↔ ¬ 𝐴𝐵)
32bicomi 225 1 𝐴𝐵𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207   = wceq 1528  wne 3016
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 208  df-ne 3017
This theorem is referenced by:  neirr  3025  necon3bd  3030  necon1d  3038  necon4d  3040  necon3ai  3041  necon4bid  3061  necon1bbii  3065  pm2.61ine  3100  pm2.61dne  3103  ne3anior  3110  sbcne12  4363  raldifsnb  4723  tpprceq3  4731  tppreqb  4732  prneimg  4779  prnebg  4780  xpeq0  6011  xpcan  6027  xpcan2  6028  fndmdifeq0  6807  ftpg  6911  fnnfpeq0  6933  suppimacnv  7832  fnsuppres  7848  ixp0  8484  isfin5-2  9802  zornn0g  9916  nn0n0n1ge2b  11952  fsuppmapnn0fiub0  13351  fsuppmapnn0ub  13353  mptnn0fsupp  13355  mptnn0fsuppr  13357  discr  13591  hashgt12el  13773  hashgt12el2  13774  hashtpg  13833  fprodle  15340  alzdvds  15660  algcvgblem  15911  lcmfunsnlem2lem2  15973  lssne0  19653  dsmm0cl  20814  pmatcollpw2lem  21315  elcls  21611  cmpfi  21946  bwth  21948  1stccnp  22000  dissnlocfin  22067  trfil3  22426  isufil2  22446  bcth3  23863  rrxmvallem  23936  mdegleb  24587  tglowdim1i  26215  tglineintmo  26356  lmieu  26498  uhgrvd00  27244  wlkon2n0  27376  wwlks  27541  rusgrnumwwlks  27681  clwwlkneq0  27735  1to2vfriswmgr  27986  numclwwlk3lem2  28091  frgrregord013  28102  nmlno0lem  28498  lnon0  28503  nmlnop0iALT  29700  atom1d  30058  uniinn0  30230  nfpconfp  30306  funcnv5mpt  30342  xaddeq0  30404  pmtrcnel  30661  fedgmullem2  30926  bnj521  31907  bnj1533  32024  bnj1541  32028  bnj1279  32188  bnj1280  32190  bnj1311  32194  spthcycl  32274  nepss  32846  bj-ismooredr2  34297  nlpineqsn  34572  poimirlem31  34805  poimirlem32  34806  itg2addnclem2  34826  ftc1anc  34857  n0elqs  35466  lfl1  36088  lkreqN  36188  pmap0  36783  paddasslem17  36854  ltrnnid  37154  dffltz  39151  ntrneikb  40324  fzdifsuc2  41457  limclr  41816  liminflbuz2  41976  fourierdlem42  42315  fourierdlem76  42348  sge0cl  42544  meadjiunlem  42628  oddprmne2  43727  mndpsuppss  44317  islininds2  44437  line2ylem  44636  line2xlem  44638  itsclc0xyqsol  44653  2itscp  44666
  Copyright terms: Public domain W3C validator