Theorem nne 2936

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 2933	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2	1	con2bii 361	. 2 ⊢ (𝐴 = 𝐵 ↔ ¬ 𝐴 ≠ 𝐵)
3	2	bicomi 227	1 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)

Syntax hints:  ¬ wn 3   ↔ wb 209   = wceq 1543   ≠ wne 2932

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 2933

This theorem is referenced by:  neirr  2941  necon3bd  2946  necon1d  2954  necon4d  2956  necon3ai  2957  necon4bid  2977  necon1bbii  2981  pm2.61ine  3015  pm2.61dne  3018  ne3anior  3025  sbcne12  4313  raldifsnb  4695  tpprceq3  4703  tppreqb  4704  prneimg  4751  prnebg  4752  xpeq0  6003  xpcan  6019  xpcan2  6020  fndmdifeq0  6842  ftpg  6949  fnnfpeq0  6971  suppimacnv  7894  fnsuppres  7911  suppcoss  7927  ixp0  8590  isfin5-2  9970  zornn0g  10084  nn0n0n1ge2b  12123  fsuppmapnn0fiub0  13531  fsuppmapnn0ub  13533  mptnn0fsupp  13535  mptnn0fsuppr  13537  discr  13772  hashgt12el  13954  hashgt12el2  13955  hashtpg  14016  fprodle  15521  alzdvds  15844  algcvgblem  16097  lcmfunsnlem2lem2  16159  lssne0  19941  dsmm0cl  20656  pmatcollpw2lem  21628  elcls  21924  cmpfi  22259  bwth  22261  1stccnp  22313  dissnlocfin  22380  trfil3  22739  isufil2  22759  bcth3  24182  rrxmvallem  24255  mdegleb  24916  tglowdim1i  26546  tglineintmo  26687  lmieu  26829  uhgrvd00  27576  wlkon2n0  27708  wwlks  27873  rusgrnumwwlks  28012  clwwlkneq0  28066  1to2vfriswmgr  28316  numclwwlk3lem2  28421  frgrregord013  28432  nmlno0lem  28828  lnon0  28833  nmlnop0iALT  30030  atom1d  30388  uniinn0  30563  nfpconfp  30640  funcnv5mpt  30679  suppiniseg  30694  xaddeq0  30750  pmtrcnel  31031  fedgmullem2  31379  zarcls1  31487  bnj521  32382  bnj1533  32499  bnj1541  32503  bnj1279  32665  bnj1280  32667  bnj1311  32671  spthcycl  32758  nepss  33331  bj-ismooredr2  34965  nlpineqsn  35265  poimirlem31  35494  poimirlem32  35495  itg2addnclem2  35515  ftc1anc  35544  n0elqs  36147  lfl1  36770  lkreqN  36870  pmap0  37465  paddasslem17  37536  ltrnnid  37836  sticksstones1  39771  dffltz  40115  ntrneikb  41322  fzdifsuc2  42463  limclr  42814  liminflbuz2  42974  fourierdlem42  43308  fourierdlem76  43341  sge0cl  43537  meadjiunlem  43621  oddprmne2  44783  mndpsuppss  45323  islininds2  45441  line2ylem  45713  line2xlem  45715  itsclc0xyqsol  45730  2itscp  45743  fdomne0  45793