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

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

Proof of Theorem nne
StepHypRef Expression
1 df-ne 2792 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
21con2bii 347 . 2 (𝐴 = 𝐵 ↔ ¬ 𝐴𝐵)
32bicomi 214 1 𝐴𝐵𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196   = wceq 1481  wne 2791
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 2792
This theorem is referenced by:  neirr  2800  necon3bd  2805  necon1d  2813  necon4d  2815  necon3ai  2816  necon4bid  2836  necon1bbii  2840  pm2.61ine  2874  pm2.61dne  2877  ne3anior  2884  sbcne12  3977  raldifsnb  4316  tpprceq3  4326  tppreqb  4327  prneimg  4379  prnebg  4380  xpeq0  5542  xpcan  5558  xpcan2  5559  funtpgOLD  5931  fndmdifeq0  6309  ftpg  6408  fnnfpeq0  6429  suppimacnv  7291  fnsuppres  7307  ixp0  7926  isfin5-2  9198  zornn0g  9312  nn0n0n1ge2b  11344  fsuppmapnn0fiub0  12776  fsuppmapnn0ub  12778  mptnn0fsupp  12780  mptnn0fsuppr  12782  discr  12984  hashgt12el  13193  hashgt12el2  13194  hashtpg  13250  fprodle  14708  alzdvds  15023  algcvgblem  15271  lcmfunsnlem2lem2  15333  lssne0  18932  dsmm0cl  20065  pmatcollpw2lem  20563  elcls  20858  cmpfi  21192  bwth  21194  1stccnp  21246  dissnlocfin  21313  trfil3  21673  isufil2  21693  bcth3  23109  rrxmvallem  23168  mdegleb  23805  tglowdim1i  25377  tglineintmo  25518  lmieu  25657  uvtxa01vtx  26279  uhgrvd00  26411  wlkon2n0  26543  wwlks  26708  rusgrnumwwlks  26850  1to2vfriswmgr  27123  numclwwlk3lem  27212  frgrregord013  27223  nmlno0lem  27618  lnon0  27623  nmlnop0iALT  28824  atom1d  29182  uniinn0  29338  funcnv5mpt  29443  xaddeq0  29492  bnj521  30779  bnj1533  30896  bnj1541  30900  bnj1279  31060  bnj1280  31062  bnj1311  31066  nepss  31574  poimirlem31  33411  poimirlem32  33412  itg2addnclem2  33433  ftc1anc  33464  lfl1  34176  lkreqN  34276  pmap0  34870  paddasslem17  34941  ltrnnid  35241  ntrneikb  38212  fzdifsuc2  39338  limclr  39687  fourierdlem42  40129  fourierdlem76  40162  sge0cl  40361  meadjiunlem  40445  oddprmne2  41389  mndpsuppss  41917  islininds2  42038
  Copyright terms: Public domain W3C validator