Theorem nne 2624

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 2620	. . 3 |- ( A =/= B <-> -. A = B )
2	1	con2bii 333	. 2 |- ( A = B <-> -. A =/= B )
3	2	bicomi 205	1 |- ( -. A =/= B <-> A = B )

Syntax hints:   -. wn 3   <-> wb 187   = wceq 1437   =/= wne 2618

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 188  df-ne 2620

This theorem is referenced by:  neirr  2628  necon3adOLD  2635  necon3bd  2636  necon2adOLD  2638  necon1bdOLD  2643  necon4adOLD  2645  necon4bdOLD  2647  necon1d  2649  necon4d  2651  necon3ai  2652  necon3biOLD  2654  necon1biOLD  2658  necon2aiOLD  2660  necon4aiOLD  2663  necon4iOLD  2669  necon4bid  2683  necon1bbii  2688  pm2.61ine  2737  pm2.61neOLD  2740  pm2.61dne  2741  ne3anior  2750  sbcne12  3803  raldifsnb  4128  tpprceq3  4137  tppreqb  4138  prneimg  4178  prnebg  4179  xpeq0  5273  xpcan  5289  xpcan2  5290  funtpg  5648  fndmdifeq0  6000  ftpg  6086  fnnfpeq0  6107  suppimacnv  6933  fnsuppres  6950  ixp0  7560  isfin5-2  8822  zornn0g  8936  nn0n0n1ge2b  10934  fsuppmapnn0fiub0  12205  fsuppmapnn0ub  12207  mptnn0fsupp  12209  mptnn0fsuppr  12211  discr  12409  hashgt12el  12593  hashgt12el2  12594  hashtpg  12638  fprodle  14038  alzdvds  14343  algcvgblem  14524  lcmfunsnlem2lem2  14600  lssne0  18162  dsmm0cl  19290  pmatcollpw2lem  19788  elcls  20076  cmpfi  20410  bwth  20412  1stccnp  20464  dissnlocfin  20531  trfil3  20890  isufil2  20910  bcth3  22286  rrxmvallem  22345  mdegleb  23000  tglowdim1i  24532  tglineintmo  24674  lmieu  24813  usgrasscusgra  25197  2pthlem2  25312  usgrcyclnl1  25354  rusgranumwlks  25670  1to2vfriswmgra  25720  numclwwlk3lem  25822  frgraregord013  25832  nmlno0lem  26420  lnon0  26425  nmlnop0iALT  27634  atom1d  27992  uniinn0  28153  funcnv5mpt  28262  xaddeq0  28324  bnj521  29541  bnj1533  29659  bnj1541  29663  bnj1279  29823  bnj1280  29825  bnj1311  29829  nepss  30346  poimirlem31  31885  poimirlem32  31886  itg2addnclem2  31908  ftc1anc  31939  lfl1  32555  lkreqN  32655  pmap0  33249  paddasslem17  33320  ltrnnid  33620  fzdifsuc2  37372  limclr  37556  fourierdlem42  37832  fourierdlem42OLD  37833  fourierdlem76  37866  sge0cl  38011  meadjiunlem  38082  mndpsuppss  39430  islininds2  39551