Theorem nne 2607

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 2603	. . 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 1369   =/= wne 2601

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 2603

This theorem is referenced by:  neirr  2608  necon3ad  2639  necon3bd  2640  necon3ai  2646  necon3bi  2647  necon1bi  2649  necon2ai  2651  necon2ad  2654  necon4ai  2665  necon4i  2666  necon4ad  2667  necon4bd  2668  necon4d  2669  necon4bid  2672  necon1bd  2674  necon1d  2675  pm2.61ne  2681  pm2.61ine  2682  pm2.61dne  2683  ne3anior  2693  sbcne12  3674  sbcne12gOLD  3675  tpprceq3  4008  tppreqb  4009  prneimg  4048  prnebg  4049  xpeq0  5253  xpcan  5269  xpcan2  5270  funtpg  5463  fndmdifeq0  5804  ftpg  5887  fnnfpeq0  5904  fnsuppresOLD  5933  suppimacnv  6696  fnsuppres  6711  ixp0  7288  elfiun  7672  isfin5-2  8552  zornn0g  8666  nn0n0n1ge2b  10636  discr  11993  hashgt12el  12165  hashgt12el2  12166  hashtpg  12178  alzdvds  13575  algcvgblem  13744  lssne0  17012  dsmm0cl  18145  elcls  18657  cmpfi  18991  bwth  18993  bwthOLD  18994  1stccnp  19046  trfil3  19441  isufil2  19461  bcth3  20822  rrxmvallem  20883  mdegleb  21515  tglowdim1i  22934  tglineintmo  23027  usgrasscusgra  23359  2pthlem2  23463  usgrcyclnl1  23494  nmlno0lem  24161  lnon0  24166  nmlnop0iALT  25367  atom1d  25725  funcnv5mpt  25956  xaddeq0  26014  sibfof  26695  nepss  27343  itg2addnclem2  28415  ftc1anc  28446  raldifsnb  30094  rusgranumwlks  30545  1to2vfriswmgra  30569  numclwwlk3lem  30672  frgraregord013  30682  mndpsuppss  30753  fsuppmapnn0ub  30765  fsuppmapnn0fiub0  30770  mptnn0fsupp  30771  pmatcollpw2lem  30862  islininds2  30949  bnj521  31657  bnj1533  31774  bnj1541  31778  bnj1279  31938  bnj1280  31940  bnj1311  31944  lfl1  32608  lkreqN  32708  pmap0  33302  paddasslem17  33373  ltrnnid  33673