Theorem nne 2944

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

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1541   ≠ wne 2940

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 2941

This theorem is referenced by:  neirr  2949  necon3bd  2954  necon1d  2962  necon4d  2964  necon3aiOLD  2966  necon4bid  2986  necon1bbii  2990  pm2.61ine  3025  ne3anior  3036  sbcne12  4411  raldifsnb  4798  tpprceq3  4806  tppreqb  4807  prneimg  4854  prnebg  4855  xpeq0  6156  xpcan  6172  xpcan2  6173  fndmdifeq0  7042  ftpg  7150  fnnfpeq0  7172  suppimacnv  8155  fnsuppres  8172  suppcoss  8188  ixp0  8921  isfin5-2  10382  zornn0g  10496  nn0n0n1ge2b  12536  fsuppmapnn0fiub0  13954  fsuppmapnn0ub  13956  mptnn0fsupp  13958  mptnn0fsuppr  13960  discr  14199  hashgt12el  14378  hashgt12el2  14379  hashtpg  14442  fprodle  15936  alzdvds  16259  algcvgblem  16510  lcmfunsnlem2lem2  16572  lssne0  20553  dsmm0cl  21286  pmatcollpw2lem  22270  elcls  22568  cmpfi  22903  bwth  22905  1stccnp  22957  dissnlocfin  23024  trfil3  23383  isufil2  23403  bcth3  24839  rrxmvallem  24912  mdegleb  25573  tglowdim1i  27741  tglineintmo  27882  lmieu  28024  uhgrvd00  28780  wlkon2n0  28912  wwlks  29078  rusgrnumwwlks  29217  clwwlkneq0  29271  1to2vfriswmgr  29521  numclwwlk3lem2  29626  frgrregord013  29637  nmlno0lem  30033  lnon0  30038  nmlnop0iALT  31235  atom1d  31593  uniinn0  31769  nfpconfp  31843  funcnv5mpt  31880  suppiniseg  31895  xaddeq0  31953  pmtrcnel  32237  fedgmullem2  32703  zarcls1  32837  bnj1533  33851  bnj1541  33855  bnj1279  34017  bnj1280  34019  bnj1311  34023  spthcycl  34108  nepss  34675  bj-ismooredr2  35979  nlpineqsn  36277  poimirlem31  36507  poimirlem32  36508  itg2addnclem2  36528  ftc1anc  36557  n0elqs  37183  lfl1  37928  lkreqN  38028  pmap0  38624  paddasslem17  38695  ltrnnid  38995  sticksstones1  40950  dffltz  41372  dflim5  42064  ntrneikb  42830  fzdifsuc2  44006  limclr  44357  liminflbuz2  44517  fourierdlem42  44851  fourierdlem76  44884  sge0cl  45083  meadjiunlem  45167  smfpimne2  45542  n0nsn2el  45721  oddprmne2  46369  mndpsuppss  47000  islininds2  47118  line2ylem  47390  line2xlem  47392  itsclc0xyqsol  47407  2itscp  47420  fdomne0  47469