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

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

Proof of Theorem nne
StepHypRef Expression
1 df-ne 3014 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
21con2bii 359 . 2 (𝐴 = 𝐵 ↔ ¬ 𝐴𝐵)
32bicomi 225 1 𝐴𝐵𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207   = wceq 1528  wne 3013
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 3014
This theorem is referenced by:  neirr  3022  necon3bd  3027  necon1d  3035  necon4d  3037  necon3ai  3038  necon4bid  3058  necon1bbii  3062  pm2.61ine  3097  pm2.61dne  3100  ne3anior  3107  sbcne12  4361  raldifsnb  4721  tpprceq3  4729  tppreqb  4730  prneimg  4777  prnebg  4778  xpeq0  6010  xpcan  6026  xpcan2  6027  fndmdifeq0  6806  ftpg  6910  fnnfpeq0  6932  suppimacnv  7830  fnsuppres  7846  ixp0  8483  isfin5-2  9801  zornn0g  9915  nn0n0n1ge2b  11951  fsuppmapnn0fiub0  13349  fsuppmapnn0ub  13351  mptnn0fsupp  13353  mptnn0fsuppr  13355  discr  13589  hashgt12el  13771  hashgt12el2  13772  hashtpg  13831  fprodle  15338  alzdvds  15658  algcvgblem  15909  lcmfunsnlem2lem2  15971  lssne0  19651  dsmm0cl  20812  pmatcollpw2lem  21313  elcls  21609  cmpfi  21944  bwth  21946  1stccnp  21998  dissnlocfin  22065  trfil3  22424  isufil2  22444  bcth3  23861  rrxmvallem  23934  mdegleb  24585  tglowdim1i  26214  tglineintmo  26355  lmieu  26497  uhgrvd00  27243  wlkon2n0  27375  wwlks  27540  rusgrnumwwlks  27680  clwwlkneq0  27734  1to2vfriswmgr  27985  numclwwlk3lem2  28090  frgrregord013  28101  nmlno0lem  28497  lnon0  28502  nmlnop0iALT  29699  atom1d  30057  uniinn0  30229  nfpconfp  30305  funcnv5mpt  30341  xaddeq0  30403  pmtrcnel  30660  fedgmullem2  30925  bnj521  31906  bnj1533  32023  bnj1541  32027  bnj1279  32187  bnj1280  32189  bnj1311  32193  spthcycl  32273  nepss  32845  bj-ismooredr2  34296  nlpineqsn  34571  poimirlem31  34804  poimirlem32  34805  itg2addnclem2  34825  ftc1anc  34856  n0elqs  35464  lfl1  36086  lkreqN  36186  pmap0  36781  paddasslem17  36852  ltrnnid  37152  dffltz  39149  ntrneikb  40322  fzdifsuc2  41453  limclr  41812  liminflbuz2  41972  fourierdlem42  42311  fourierdlem76  42344  sge0cl  42540  meadjiunlem  42624  oddprmne2  43757  mndpsuppss  44347  islininds2  44467  line2ylem  44666  line2xlem  44668  itsclc0xyqsol  44683  2itscp  44696
  Copyright terms: Public domain W3C validator