Theorem nne 2968

Description: Negation of inequality. (Contributed by NM, 9-Jun-2006.)

Assertion

Ref	Expression
nne	⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)

Proof of Theorem nne

Step	Hyp	Ref	Expression
1		df-ne 2965	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2	1	con2bii 360	. 2 ⊢ (𝐴 = 𝐵 ↔ ¬ 𝐴 ≠ 𝐵)
3	2	bicomi 227	1 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)

Syntax hints:  ¬ wn 3   ↔ wb 209   = wceq 1567   ≠ wne 2964

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 210  df-ne 2965

This theorem is referenced by:  neirr  2973  necon3bd  2978  necon1d  2986  necon4d  2988  necon4bid  3009  necon1bbii  3013  pm2.61ine  3047  ne3anior  3058  sbcne12  4386  raldifsnb  4768  tpprceq3  4776  tppreqb  4777  prneimg  4823  prnebg  4825  xpeq0  6158  xpcan  6175  xpcan2  6176  fndmdifeq0  7040  ftpg  7154  fnnfpeq0  7177  suppimacnv  8169  fnsuppres  8186  suppcoss  8202  ixp0  8928  isfin5-2  10374  zornn0g  10488  nn0n0n1ge2b  12572  fsuppmapnn0fiub0  14028  fsuppmapnn0ub  14030  mptnn0fsupp  14032  mptnn0fsuppr  14034  discr  14275  hashgt12el  14458  hashgt12el2  14459  hashtpg  14521  hash3tpde  14529  fprodle  16049  alzdvds  16377  algcvgblem  16634  lcmfunsnlem2lem2  16696  mndpsuppss  18822  lssne0  21049  dsmm0cl  21858  pmatcollpw2lem  22902  elcls  23198  cmpfi  23533  bwth  23535  1stccnp  23587  dissnlocfin  23654  trfil3  24013  isufil2  24033  bcth3  25458  rrxmvallem  25531  mdegleb  26189  tglowdim1i  28735  tglineintmo  28876  lmieu  29050  uhgrvd00  29824  wlkon2n0  29954  wwlks  30124  rusgrnumwwlks  30266  clwwlkneq0  30320  1to2vfriswmgr  30570  numclwwlk3lem2  30675  frgrregord013  30686  nmlno0lem  31085  lnon0  31090  nmlnop0iALT  32287  atom1d  32645  n0nsnel  32801  uniinn0  32837  nfpconfp  32917  funcnv5mpt  32952  suppiniseg  32971  xaddeq0  33038  pmtrcnel  33349  1arithidom  33771  esplymhp  33902  fedgmullem2  33964  irredminply  34050  zarcls1  34203  bnj1533  35184  bnj1541  35188  bnj1279  35350  bnj1280  35352  bnj1311  35356  spthcycl  35519  nepss  36108  ttcwf2  36924  bj-ismooredr2  37639  nlpineqsn  37941  poimirlem31  38189  poimirlem32  38190  itg2addnclem2  38210  ftc1anc  38239  n0elqs  38870  suceldisj  39356  lfl1  39733  lkreqN  39833  pmap0  40428  paddasslem17  40499  ltrnnid  40799  sticksstones1  42802  dffltz  43257  dflim5  43947  ntrneikb  44711  fzdifsuc2  45920  limclr  46260  liminflbuz2  46420  fourierdlem42  46754  fourierdlem76  46787  sge0cl  46986  meadjiunlem  47070  smfpimne2  47445  chnerlem1  47489  n0nsn2el  47650  oddprmne2  48368  usgrexmpl2trifr  48690  islininds2  49148  line2ylem  49415  line2xlem  49417  itsclc0xyqsol  49432  2itscp  49445  dmrnxp  49499  fdomne0  49512  oppcendc  49680