Theorem nne 2661

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 2657	. . 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 1374   =/= wne 2655

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 2657

This theorem is referenced by:  neirr  2664  necon3adOLD  2671  necon3bd  2672  necon2adOLD  2674  necon1bdOLD  2679  necon4adOLD  2681  necon4bdOLD  2683  necon1d  2685  necon4d  2687  necon3ai  2688  necon3biOLD  2690  necon1biOLD  2694  necon2aiOLD  2696  necon4aiOLD  2699  necon4iOLD  2705  necon4bid  2719  necon1bbii  2724  pm2.61ine  2773  pm2.61neOLD  2776  pm2.61dne  2777  ne3anior  2786  sbcne12  3820  sbcne12gOLD  3821  raldifsnb  4151  tpprceq3  4160  tppreqb  4161  prneimg  4200  prnebg  4201  xpeq0  5418  xpcan  5434  xpcan2  5435  funtpg  5629  fndmdifeq0  5978  ftpg  6062  fnnfpeq0  6083  fnsuppresOLD  6112  suppimacnv  6902  fnsuppres  6917  ixp0  7492  elfiun  7879  isfin5-2  8760  zornn0g  8874  nn0n0n1ge2b  10849  fsuppmapnn0fiub0  12055  fsuppmapnn0ub  12057  mptnn0fsupp  12059  mptnn0fsuppr  12061  discr  12258  hashgt12el  12433  hashgt12el2  12434  hashtpg  12476  alzdvds  13884  algcvgblem  14054  lssne0  17373  dsmm0cl  18531  pmatcollpw2lem  19038  elcls  19333  cmpfi  19667  bwth  19669  bwthOLD  19670  1stccnp  19722  trfil3  20117  isufil2  20137  bcth3  21498  rrxmvallem  21559  mdegleb  22192  tglowdim1i  23613  tglineintmo  23728  lmieu  23820  usgrasscusgra  24145  2pthlem2  24260  usgrcyclnl1  24302  rusgranumwlks  24618  nmlno0lem  25234  lnon0  25239  nmlnop0iALT  26440  atom1d  26798  funcnv5mpt  27033  xaddeq0  27091  sibfof  27772  nepss  28420  itg2addnclem2  29495  ftc1anc  29526  limclr  31016  fourierdlem42  31268  fourierdlem76  31302  1to2vfriswmgra  31724  numclwwlk3lem  31827  frgraregord013  31837  mndpsuppss  31912  islininds2  32033  bnj521  32747  bnj1533  32864  bnj1541  32868  bnj1279  33028  bnj1280  33030  bnj1311  33034  lfl1  33742  lkreqN  33842  pmap0  34436  paddasslem17  34507  ltrnnid  34807