Theorem nne 2929

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 2926	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2	1	con2bii 357	. 2 ⊢ (𝐴 = 𝐵 ↔ ¬ 𝐴 ≠ 𝐵)
3	2	bicomi 224	1 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1540   ≠ wne 2925

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 207  df-ne 2926

This theorem is referenced by:  neirr  2934  necon3bd  2939  necon1d  2947  necon4d  2949  necon4bid  2970  necon1bbii  2974  pm2.61ine  3008  ne3anior  3019  sbcne12  4378  raldifsnb  4760  tpprceq3  4768  tppreqb  4769  prneimg  4818  prnebg  4820  xpeq0  6133  xpcan  6149  xpcan2  6150  fndmdifeq0  7016  ftpg  7128  fnnfpeq0  7152  suppimacnv  8153  fnsuppres  8170  suppcoss  8186  ixp0  8904  isfin5-2  10344  zornn0g  10458  nn0n0n1ge2b  12511  fsuppmapnn0fiub0  13958  fsuppmapnn0ub  13960  mptnn0fsupp  13962  mptnn0fsuppr  13964  discr  14205  hashgt12el  14387  hashgt12el2  14388  hashtpg  14450  hash3tpde  14458  fprodle  15962  alzdvds  16290  algcvgblem  16547  lcmfunsnlem2lem2  16609  mndpsuppss  18692  lssne0  20857  dsmm0cl  21649  pmatcollpw2lem  22664  elcls  22960  cmpfi  23295  bwth  23297  1stccnp  23349  dissnlocfin  23416  trfil3  23775  isufil2  23795  bcth3  25231  rrxmvallem  25304  mdegleb  25969  tglowdim1i  28428  tglineintmo  28569  lmieu  28711  uhgrvd00  29462  wlkon2n0  29594  wwlks  29765  rusgrnumwwlks  29904  clwwlkneq0  29958  1to2vfriswmgr  30208  numclwwlk3lem2  30313  frgrregord013  30324  nmlno0lem  30722  lnon0  30727  nmlnop0iALT  31924  atom1d  32282  n0nsnel  32444  uniinn0  32479  nfpconfp  32556  funcnv5mpt  32592  suppiniseg  32609  xaddeq0  32676  pmtrcnel  33046  1arithidom  33508  fedgmullem2  33626  irredminply  33706  zarcls1  33859  bnj1533  34842  bnj1541  34846  bnj1279  35008  bnj1280  35010  bnj1311  35014  spthcycl  35116  nepss  35705  bj-ismooredr2  37098  nlpineqsn  37396  poimirlem31  37645  poimirlem32  37646  itg2addnclem2  37666  ftc1anc  37695  n0elqs  38314  lfl1  39063  lkreqN  39163  pmap0  39759  paddasslem17  39830  ltrnnid  40130  sticksstones1  42134  dffltz  42622  dflim5  43318  ntrneikb  44083  fzdifsuc2  45308  limclr  45653  liminflbuz2  45813  fourierdlem42  46147  fourierdlem76  46180  sge0cl  46379  meadjiunlem  46463  smfpimne2  46838  n0nsn2el  47026  oddprmne2  47716  usgrexmpl2trifr  48028  islininds2  48473  line2ylem  48740  line2xlem  48742  itsclc0xyqsol  48757  2itscp  48770  dmrnxp  48825  fdomne0  48838  oppcendc  49007