Theorem nne 2602

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 2598	. . 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 1362   =/= wne 2596

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 2598

This theorem is referenced by:  neirr  2603  necon3ad  2634  necon3bd  2635  necon3ai  2641  necon3bi  2642  necon1bi  2644  necon2ai  2646  necon2ad  2649  necon4ai  2660  necon4i  2661  necon4ad  2662  necon4bd  2663  necon4d  2664  necon4bid  2667  necon1bd  2669  necon1d  2670  pm2.61ne  2676  pm2.61ine  2677  pm2.61dne  2678  ne3anior  2688  sbcne12  3667  sbcne12gOLD  3668  tpprceq3  4001  tppreqb  4002  prneimg  4041  prnebg  4042  xpeq0  5246  xpcan  5262  xpcan2  5263  funtpg  5456  fndmdifeq0  5797  ftpg  5879  fnnfpeq0  5896  fnsuppresOLD  5925  suppimacnv  6690  fnsuppres  6705  ixp0  7284  elfiun  7668  isfin5-2  8548  zornn0g  8662  nn0n0n1ge2b  10631  discr  11984  hashgt12el  12156  hashgt12el2  12157  hashtpg  12169  alzdvds  13565  algcvgblem  13734  lssne0  16953  dsmm0cl  18006  elcls  18518  cmpfi  18852  bwth  18854  bwthOLD  18855  1stccnp  18907  trfil3  19302  isufil2  19322  bcth3  20683  rrxmvallem  20744  mdegleb  21419  tglowdim1i  22835  tglineintmo  22916  usgrasscusgra  23213  2pthlem2  23317  usgrcyclnl1  23348  nmlno0lem  24015  lnon0  24020  nmlnop0iALT  25221  atom1d  25579  funcnv5mpt  25811  xaddeq0  25870  sibfof  26573  nepss  27220  itg2addnclem2  28285  ftc1anc  28316  raldifsnb  29966  rusgranumwlks  30417  1to2vfriswmgra  30441  numclwwlk3lem  30544  frgraregord013  30554  mndpsuppss  30612  islininds2  30724  bnj521  31427  bnj1533  31544  bnj1541  31548  bnj1279  31708  bnj1280  31710  bnj1311  31714  lfl1  32285  lkreqN  32385  pmap0  32979  paddasslem17  33050  ltrnnid  33350