Theorem nne 2658

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 2654	. . 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 1395   =/= wne 2652

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 2654

This theorem is referenced by:  neirr  2661  necon3adOLD  2668  necon3bd  2669  necon2adOLD  2671  necon1bdOLD  2676  necon4adOLD  2678  necon4bdOLD  2680  necon1d  2682  necon4d  2684  necon3ai  2685  necon3biOLD  2687  necon1biOLD  2691  necon2aiOLD  2693  necon4aiOLD  2696  necon4iOLD  2702  necon4bid  2716  necon1bbii  2721  pm2.61ine  2770  pm2.61neOLD  2773  pm2.61dne  2774  ne3anior  2783  sbcne12  3836  raldifsnb  4163  tpprceq3  4172  tppreqb  4173  prneimg  4213  prnebg  4214  xpeq0  5434  xpcan  5450  xpcan2  5451  funtpg  5644  fndmdifeq0  5994  ftpg  6082  fnnfpeq0  6103  fnsuppresOLD  6132  suppimacnv  6928  fnsuppres  6945  ixp0  7521  isfin5-2  8788  zornn0g  8902  nn0n0n1ge2b  10881  fsuppmapnn0fiub0  12102  fsuppmapnn0ub  12104  mptnn0fsupp  12106  mptnn0fsuppr  12108  discr  12306  hashgt12el  12485  hashgt12el2  12486  hashtpg  12527  alzdvds  14048  algcvgblem  14218  lssne0  17724  dsmm0cl  18898  pmatcollpw2lem  19405  elcls  19701  cmpfi  20035  bwth  20037  1stccnp  20089  dissnlocfin  20156  trfil3  20515  isufil2  20535  bcth3  21896  rrxmvallem  21957  mdegleb  22590  tglowdim1i  24018  tglineintmo  24148  lmieu  24276  usgrasscusgra  24610  2pthlem2  24725  usgrcyclnl1  24767  rusgranumwlks  25083  1to2vfriswmgra  25133  numclwwlk3lem  25235  frgraregord013  25245  nmlno0lem  25835  lnon0  25840  nmlnop0iALT  27041  atom1d  27399  uniinn0  27559  funcnv5mpt  27665  xaddeq0  27730  nepss  29313  itg2addnclem2  30272  ftc1anc  30303  fzdifsuc2  31715  fprodle  31807  limclr  31864  fourierdlem42  32134  fourierdlem76  32168  mndpsuppss  33108  islininds2  33229  bnj521  33935  bnj1533  34053  bnj1541  34057  bnj1279  34217  bnj1280  34219  bnj1311  34223  lfl1  34938  lkreqN  35038  pmap0  35632  paddasslem17  35703  ltrnnid  36003