Theorem nne 2947

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 2944	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2	1	con2bii 358	. 2 ⊢ (𝐴 = 𝐵 ↔ ¬ 𝐴 ≠ 𝐵)
3	2	bicomi 223	1 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1539   ≠ wne 2943

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 206  df-ne 2944

This theorem is referenced by:  neirr  2952  necon3bd  2957  necon1d  2965  necon4d  2967  necon3aiOLD  2969  necon4bid  2989  necon1bbii  2993  pm2.61ine  3028  ne3anior  3038  sbcne12  4348  raldifsnb  4731  tpprceq3  4739  tppreqb  4740  prneimg  4787  prnebg  4788  xpeq0  6065  xpcan  6081  xpcan2  6082  fndmdifeq0  6923  ftpg  7030  fnnfpeq0  7052  suppimacnv  7988  fnsuppres  8005  suppcoss  8021  ixp0  8717  isfin5-2  10145  zornn0g  10259  nn0n0n1ge2b  12299  fsuppmapnn0fiub0  13711  fsuppmapnn0ub  13713  mptnn0fsupp  13715  mptnn0fsuppr  13717  discr  13953  hashgt12el  14135  hashgt12el2  14136  hashtpg  14197  fprodle  15704  alzdvds  16027  algcvgblem  16280  lcmfunsnlem2lem2  16342  lssne0  20210  dsmm0cl  20945  pmatcollpw2lem  21924  elcls  22222  cmpfi  22557  bwth  22559  1stccnp  22611  dissnlocfin  22678  trfil3  23037  isufil2  23057  bcth3  24493  rrxmvallem  24566  mdegleb  25227  tglowdim1i  26860  tglineintmo  27001  lmieu  27143  uhgrvd00  27899  wlkon2n0  28032  wwlks  28197  rusgrnumwwlks  28336  clwwlkneq0  28390  1to2vfriswmgr  28640  numclwwlk3lem2  28745  frgrregord013  28756  nmlno0lem  29152  lnon0  29157  nmlnop0iALT  30354  atom1d  30712  uniinn0  30887  nfpconfp  30964  funcnv5mpt  31002  suppiniseg  31017  xaddeq0  31073  pmtrcnel  31355  fedgmullem2  31708  zarcls1  31816  bnj521  32713  bnj1533  32829  bnj1541  32833  bnj1279  32995  bnj1280  32997  bnj1311  33001  spthcycl  33088  nepss  33659  bj-ismooredr2  35278  nlpineqsn  35576  poimirlem31  35805  poimirlem32  35806  itg2addnclem2  35826  ftc1anc  35855  n0elqs  36458  lfl1  37081  lkreqN  37181  pmap0  37776  paddasslem17  37847  ltrnnid  38147  sticksstones1  40099  dffltz  40468  ntrneikb  41674  fzdifsuc2  42819  limclr  43166  liminflbuz2  43326  fourierdlem42  43660  fourierdlem76  43693  sge0cl  43889  meadjiunlem  43973  oddprmne2  45134  mndpsuppss  45674  islininds2  45792  line2ylem  46064  line2xlem  46066  itsclc0xyqsol  46081  2itscp  46094  fdomne0  46144