Theorem nne 2642

Description: Negation of inequality. (Contributed by NM, 9-Jun-2006.)

Assertion

Ref	Expression
nne	|- ( -. A =/= B <-> A = B )

Proof of Theorem nne

Step	Hyp	Ref	Expression
1		df-ne 2638	. . 3 |- ( A =/= B <-> -. A = B )
2	1	con2bii 332	. 2 |- ( A = B <-> -. A =/= B )
3	2	bicomi 202	1 |- ( -. A =/= B <-> A = B )

Syntax hints:   -. wn 3   <-> wb 184   = wceq 1381   =/= wne 2636

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 185  df-ne 2638

This theorem is referenced by:  neirr  2645  necon3adOLD  2652  necon3bd  2653  necon2adOLD  2655  necon1bdOLD  2660  necon4adOLD  2662  necon4bdOLD  2664  necon1d  2666  necon4d  2668  necon3ai  2669  necon3biOLD  2671  necon1biOLD  2675  necon2aiOLD  2677  necon4aiOLD  2680  necon4iOLD  2686  necon4bid  2700  necon1bbii  2705  pm2.61ine  2754  pm2.61neOLD  2757  pm2.61dne  2758  ne3anior  2767  sbcne12  3809  sbcne12gOLD  3810  raldifsnb  4142  tpprceq3  4151  tppreqb  4152  prneimg  4192  prnebg  4193  xpeq0  5413  xpcan  5429  xpcan2  5430  funtpg  5624  fndmdifeq0  5974  ftpg  6062  fnnfpeq0  6083  fnsuppresOLD  6112  suppimacnv  6910  fnsuppres  6925  ixp0  7500  isfin5-2  8769  zornn0g  8883  nn0n0n1ge2b  10861  fsuppmapnn0fiub0  12073  fsuppmapnn0ub  12075  mptnn0fsupp  12077  mptnn0fsuppr  12079  discr  12277  hashgt12el  12455  hashgt12el2  12456  hashtpg  12497  alzdvds  13908  algcvgblem  14078  lssne0  17465  dsmm0cl  18638  pmatcollpw2lem  19145  elcls  19440  cmpfi  19774  bwth  19776  bwthOLD  19777  1stccnp  19829  dissnlocfin  19896  trfil3  20255  isufil2  20275  bcth3  21636  rrxmvallem  21697  mdegleb  22330  tglowdim1i  23757  tglineintmo  23887  lmieu  24015  usgrasscusgra  24348  2pthlem2  24463  usgrcyclnl1  24505  rusgranumwlks  24821  1to2vfriswmgra  24871  numclwwlk3lem  24973  frgraregord013  24983  nmlno0lem  25573  lnon0  25578  nmlnop0iALT  26779  atom1d  27137  uniinn0  27289  funcnv5mpt  27376  xaddeq0  27438  nepss  28961  itg2addnclem2  30035  ftc1anc  30066  limclr  31565  fourierdlem42  31816  fourierdlem76  31850  mndpsuppss  32674  islininds2  32795  bnj521  33500  bnj1533  33617  bnj1541  33621  bnj1279  33781  bnj1280  33783  bnj1311  33787  lfl1  34497  lkreqN  34597  pmap0  35191  paddasslem17  35262  ltrnnid  35562