Theorem nne 2639

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 2635	. . 3 |- ( A =/= B <-> -. A = B )
2	1	con2bii 338	. 2 |- ( A = B <-> -. A =/= B )
3	2	bicomi 207	1 |- ( -. A =/= B <-> A = B )

Syntax hints:   -. wn 3   <-> wb 189   = wceq 1455   =/= wne 2633

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 190  df-ne 2635

This theorem is referenced by:  neirr  2644  necon3bd  2650  necon1d  2658  necon4d  2660  necon3ai  2661  necon4bid  2681  necon1bbii  2685  pm2.61ine  2719  pm2.61dne  2722  ne3anior  2729  sbcne12  3787  raldifsnb  4116  tpprceq3  4125  tppreqb  4126  prneimg  4170  prnebg  4171  xpeq0  5276  xpcan  5292  xpcan2  5293  funtpg  5651  fndmdifeq0  6011  ftpg  6098  fnnfpeq0  6119  suppimacnv  6952  fnsuppres  6969  ixp0  7581  isfin5-2  8847  zornn0g  8961  nn0n0n1ge2b  10962  fsuppmapnn0fiub0  12237  fsuppmapnn0ub  12239  mptnn0fsupp  12241  mptnn0fsuppr  12243  discr  12441  hashgt12el  12628  hashgt12el2  12629  hashtpg  12674  fprodle  14099  alzdvds  14404  algcvgblem  14585  lcmfunsnlem2lem2  14661  lssne0  18223  dsmm0cl  19352  pmatcollpw2lem  19850  elcls  20138  cmpfi  20472  bwth  20474  1stccnp  20526  dissnlocfin  20593  trfil3  20952  isufil2  20972  bcth3  22348  rrxmvallem  22407  mdegleb  23062  tglowdim1i  24594  tglineintmo  24736  lmieu  24875  usgrasscusgra  25260  2pthlem2  25375  usgrcyclnl1  25417  rusgranumwlks  25733  1to2vfriswmgra  25783  numclwwlk3lem  25885  frgraregord013  25895  nmlno0lem  26483  lnon0  26488  nmlnop0iALT  27697  atom1d  28055  uniinn0  28212  funcnv5mpt  28321  xaddeq0  28379  bnj521  29594  bnj1533  29712  bnj1541  29716  bnj1279  29876  bnj1280  29878  bnj1311  29882  nepss  30399  poimirlem31  32016  poimirlem32  32017  itg2addnclem2  32039  ftc1anc  32070  lfl1  32681  lkreqN  32781  pmap0  33375  paddasslem17  33446  ltrnnid  33746  fzdifsuc2  37568  limclr  37774  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem76  38084  sge0cl  38261  meadjiunlem  38341  uvtxa01vtx  39520  uhgrvd00  39621  mndpsuppss  40429  islininds2  40550