Theorem nne 2604

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 2600	. . 3 |- ( A =/= B <-> -. A = B )
2	1	con2bii 330	. 2 |- ( A = B <-> -. A =/= B )
3	2	bicomi 202	1 |- ( -. A =/= B <-> A = B )

Syntax hints:   -. wn 3   <-> wb 184   = wceq 1405   =/= wne 2598

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 2600

This theorem is referenced by:  neirr  2607  necon3adOLD  2614  necon3bd  2615  necon2adOLD  2617  necon1bdOLD  2622  necon4adOLD  2624  necon4bdOLD  2626  necon1d  2628  necon4d  2630  necon3ai  2631  necon3biOLD  2633  necon1biOLD  2637  necon2aiOLD  2639  necon4aiOLD  2642  necon4iOLD  2648  necon4bid  2662  necon1bbii  2667  pm2.61ine  2716  pm2.61neOLD  2719  pm2.61dne  2720  ne3anior  2729  sbcne12  3780  raldifsnb  4103  tpprceq3  4112  tppreqb  4113  prneimg  4153  prnebg  4154  xpeq0  5245  xpcan  5261  xpcan2  5262  funtpg  5619  fndmdifeq0  5971  ftpg  6061  fnnfpeq0  6082  fnsuppresOLD  6113  suppimacnv  6913  fnsuppres  6930  ixp0  7540  isfin5-2  8803  zornn0g  8917  nn0n0n1ge2b  10901  fsuppmapnn0fiub0  12143  fsuppmapnn0ub  12145  mptnn0fsupp  12147  mptnn0fsuppr  12149  discr  12347  hashgt12el  12530  hashgt12el2  12531  hashtpg  12572  alzdvds  14245  algcvgblem  14415  lssne0  17917  dsmm0cl  19069  pmatcollpw2lem  19570  elcls  19867  cmpfi  20201  bwth  20203  1stccnp  20255  dissnlocfin  20322  trfil3  20681  isufil2  20701  bcth3  22062  rrxmvallem  22123  mdegleb  22756  tglowdim1i  24273  tglineintmo  24407  lmieu  24540  usgrasscusgra  24900  2pthlem2  25015  usgrcyclnl1  25057  rusgranumwlks  25373  1to2vfriswmgra  25423  numclwwlk3lem  25525  frgraregord013  25535  nmlno0lem  26122  lnon0  26127  nmlnop0iALT  27327  atom1d  27685  uniinn0  27845  funcnv5mpt  27954  xaddeq0  28014  bnj521  29119  bnj1533  29237  bnj1541  29241  bnj1279  29401  bnj1280  29403  bnj1311  29407  nepss  29924  itg2addnclem2  31440  ftc1anc  31471  lfl1  32088  lkreqN  32188  pmap0  32782  paddasslem17  32853  ltrnnid  33153  fzdifsuc2  36881  fprodle  36972  limclr  37029  fourierdlem42  37299  fourierdlem76  37333  mndpsuppss  38475  islininds2  38596