Theorem nne 2650

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 2646	. . 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 1370   =/= wne 2644

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 2646

This theorem is referenced by:  neirr  2653  necon3adOLD  2659  necon3bd  2660  necon2adOLD  2662  necon1bdOLD  2667  necon4adOLD  2669  necon4bdOLD  2671  necon1d  2673  necon4d  2675  necon3ai  2676  necon3biOLD  2678  necon1biOLD  2682  necon2aiOLD  2684  necon4aiOLD  2687  necon4iOLD  2693  necon4bid  2707  necon1bbii  2712  pm2.61ine  2761  pm2.61neOLD  2764  pm2.61dne  2765  ne3anior  2774  sbcne12  3777  sbcne12gOLD  3778  tpprceq3  4111  tppreqb  4112  prneimg  4151  prnebg  4152  xpeq0  5356  xpcan  5372  xpcan2  5373  funtpg  5566  fndmdifeq0  5908  ftpg  5991  fnnfpeq0  6008  fnsuppresOLD  6037  suppimacnv  6801  fnsuppres  6816  ixp0  7396  elfiun  7781  isfin5-2  8661  zornn0g  8775  nn0n0n1ge2b  10745  discr  12102  hashgt12el  12275  hashgt12el2  12276  hashtpg  12288  alzdvds  13685  algcvgblem  13854  lssne0  17138  dsmm0cl  18274  elcls  18793  cmpfi  19127  bwth  19129  bwthOLD  19130  1stccnp  19182  trfil3  19577  isufil2  19597  bcth3  20958  rrxmvallem  21019  mdegleb  21651  tglowdim1i  23072  tglineintmo  23169  usgrasscusgra  23526  2pthlem2  23630  usgrcyclnl1  23661  nmlno0lem  24328  lnon0  24333  nmlnop0iALT  25534  atom1d  25892  funcnv5mpt  26122  xaddeq0  26180  sibfof  26860  nepss  27508  itg2addnclem2  28582  ftc1anc  28613  raldifsnb  30261  rusgranumwlks  30712  1to2vfriswmgra  30736  numclwwlk3lem  30839  frgraregord013  30849  mndpsuppss  30922  fsuppmapnn0ub  30934  fsuppmapnn0fiub0  30939  mptnn0fsupp  30940  mptnn0fsuppr  30941  islininds2  31125  pmatcollpwlem  31233  bnj521  32028  bnj1533  32145  bnj1541  32149  bnj1279  32309  bnj1280  32311  bnj1311  32315  lfl1  33021  lkreqN  33121  pmap0  33715  paddasslem17  33786  ltrnnid  34086