Theorem nne 2945

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

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1542   ≠ wne 2941

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 2942

This theorem is referenced by:  neirr  2950  necon3bd  2955  necon1d  2963  necon4d  2965  necon3aiOLD  2967  necon4bid  2987  necon1bbii  2991  pm2.61ine  3026  ne3anior  3037  sbcne12  4413  raldifsnb  4800  tpprceq3  4808  tppreqb  4809  prneimg  4856  prnebg  4857  xpeq0  6160  xpcan  6176  xpcan2  6177  fndmdifeq0  7046  ftpg  7154  fnnfpeq0  7176  suppimacnv  8159  fnsuppres  8176  suppcoss  8192  ixp0  8925  isfin5-2  10386  zornn0g  10500  nn0n0n1ge2b  12540  fsuppmapnn0fiub0  13958  fsuppmapnn0ub  13960  mptnn0fsupp  13962  mptnn0fsuppr  13964  discr  14203  hashgt12el  14382  hashgt12el2  14383  hashtpg  14446  fprodle  15940  alzdvds  16263  algcvgblem  16514  lcmfunsnlem2lem2  16576  lssne0  20561  dsmm0cl  21295  pmatcollpw2lem  22279  elcls  22577  cmpfi  22912  bwth  22914  1stccnp  22966  dissnlocfin  23033  trfil3  23392  isufil2  23412  bcth3  24848  rrxmvallem  24921  mdegleb  25582  tglowdim1i  27752  tglineintmo  27893  lmieu  28035  uhgrvd00  28791  wlkon2n0  28923  wwlks  29089  rusgrnumwwlks  29228  clwwlkneq0  29282  1to2vfriswmgr  29532  numclwwlk3lem2  29637  frgrregord013  29648  nmlno0lem  30046  lnon0  30051  nmlnop0iALT  31248  atom1d  31606  uniinn0  31782  nfpconfp  31856  funcnv5mpt  31893  suppiniseg  31908  xaddeq0  31966  pmtrcnel  32250  fedgmullem2  32715  zarcls1  32849  bnj1533  33863  bnj1541  33867  bnj1279  34029  bnj1280  34031  bnj1311  34035  spthcycl  34120  nepss  34687  bj-ismooredr2  35991  nlpineqsn  36289  poimirlem31  36519  poimirlem32  36520  itg2addnclem2  36540  ftc1anc  36569  n0elqs  37195  lfl1  37940  lkreqN  38040  pmap0  38636  paddasslem17  38707  ltrnnid  39007  sticksstones1  40962  dffltz  41376  dflim5  42079  ntrneikb  42845  fzdifsuc2  44020  limclr  44371  liminflbuz2  44531  fourierdlem42  44865  fourierdlem76  44898  sge0cl  45097  meadjiunlem  45181  smfpimne2  45556  n0nsn2el  45735  oddprmne2  46383  mndpsuppss  47047  islininds2  47165  line2ylem  47437  line2xlem  47439  itsclc0xyqsol  47454  2itscp  47467  fdomne0  47516