Theorem nne 2658

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

Assertion

Ref	Expression
nne

Proof of Theorem nne

Step	Hyp	Ref	Expression
1		df-ne 2654	. . 3
2	1	con2bii 332	. 2
3	2	bicomi 202	1

Syntax hints:  -.wn 3  <->wb 184  =wceq 1395  =/=wne 2652

This theorem is referenced by:  neirr  2661  necon3adOLD  2668  necon3bd  2669  necon2adOLD  2671  necon1bdOLD  2676  necon4adOLD  2678  necon4bdOLD  2680  necon1d  2682  necon4d  2684  necon3ai  2685  necon3biOLD  2687  necon1biOLD  2691  necon2aiOLD  2693  necon4aiOLD  2696  necon4iOLD  2702  necon4bid  2716  necon1bbii  2721  pm2.61ine  2770  pm2.61neOLD  2773  pm2.61dne  2774  ne3anior  2783  sbcne12  3827  sbcne12gOLD  3828  raldifsnb  4161  tpprceq3  4170  tppreqb  4171  prneimg  4211  prnebg  4212  xpeq0  5432  xpcan  5448  xpcan2  5449  funtpg  5643  fndmdifeq0  5993  ftpg  6081  fnnfpeq0  6102  fnsuppresOLD  6131  suppimacnv  6929  fnsuppres  6946  ixp0  7522  isfin5-2  8792  zornn0g  8906  nn0n0n1ge2b  10885  fsuppmapnn0fiub0  12099  fsuppmapnn0ub  12101  mptnn0fsupp  12103  mptnn0fsuppr  12105  discr  12303  hashgt12el  12481  hashgt12el2  12482  hashtpg  12523  alzdvds  14036  algcvgblem  14206  lssne0  17597  dsmm0cl  18771  pmatcollpw2lem  19278  elcls  19574  cmpfi  19908  bwth  19910  bwthOLD  19911  1stccnp  19963  dissnlocfin  20030  trfil3  20389  isufil2  20409  bcth3  21770  rrxmvallem  21831  mdegleb  22464  tglowdim1i  23892  tglineintmo  24022  lmieu  24150  usgrasscusgra  24483  2pthlem2  24598  usgrcyclnl1  24640  rusgranumwlks  24956  1to2vfriswmgra  25006  numclwwlk3lem  25108  frgraregord013  25118  nmlno0lem  25708  lnon0  25713  nmlnop0iALT  26914  atom1d  27272  uniinn0  27424  funcnv5mpt  27511  xaddeq0  27573  nepss  29095  itg2addnclem2  30067  ftc1anc  30098  fzdifsuc2  31512  fprodle  31604  limclr  31661  fourierdlem42  31931  fourierdlem76  31965  mndpsuppss  32964  islininds2  33085  bnj521  33792  bnj1533  33910  bnj1541  33914  bnj1279  34074  bnj1280  34076  bnj1311  34080  lfl1  34795  lkreqN  34895  pmap0  35489  paddasslem17  35560  ltrnnid  35860

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 2654