Theorem nne 2971

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 2968	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2	1	con2bii 350	. 2 ⊢ (𝐴 = 𝐵 ↔ ¬ 𝐴 ≠ 𝐵)
3	2	bicomi 216	1 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)

Syntax hints:  ¬ wn 3   ↔ wb 198   = wceq 1507   ≠ wne 2967

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 199  df-ne 2968

This theorem is referenced by:  neirr  2976  necon3bd  2981  necon1d  2989  necon4d  2991  necon3ai  2992  necon4bid  3012  necon1bbii  3016  pm2.61ine  3051  pm2.61dne  3054  ne3anior  3061  sbcne12  4251  raldifsnb  4604  tpprceq3  4612  tppreqb  4613  prneimg  4660  prnebg  4661  xpeq0  5859  xpcan  5875  xpcan2  5876  fndmdifeq0  6641  ftpg  6743  fnnfpeq0  6765  suppimacnv  7646  fnsuppres  7662  ixp0  8294  isfin5-2  9613  zornn0g  9727  nn0n0n1ge2b  11778  fsuppmapnn0fiub0  13179  fsuppmapnn0ub  13181  mptnn0fsupp  13183  mptnn0fsuppr  13185  discr  13419  hashgt12el  13599  hashgt12el2  13600  hashtpg  13657  fprodle  15213  alzdvds  15533  algcvgblem  15780  lcmfunsnlem2lem2  15842  lssne0  19447  dsmm0cl  20589  pmatcollpw2lem  21092  elcls  21388  cmpfi  21723  bwth  21725  1stccnp  21777  dissnlocfin  21844  trfil3  22203  isufil2  22223  bcth3  23640  rrxmvallem  23713  mdegleb  24364  tglowdim1i  25992  tglineintmo  26133  lmieu  26275  uhgrvd00  27022  wlkon2n0  27153  wwlks  27324  rusgrnumwwlks  27483  rusgrnumwwlksOLD  27484  clwwlkneq0  27547  1to2vfriswmgr  27816  numclwwlk3lem2  27944  frgrregord013  27955  nmlno0lem  28350  lnon0  28355  nmlnop0iALT  29556  atom1d  29914  uniinn0  30073  funcnv5mpt  30178  xaddeq0  30232  fedgmullem2  30655  bnj521  31655  bnj1533  31771  bnj1541  31775  bnj1279  31935  bnj1280  31937  bnj1311  31941  nepss  32468  nlpineqsn  34130  poimirlem31  34364  poimirlem32  34365  itg2addnclem2  34385  ftc1anc  34416  n0elqs  35028  lfl1  35651  lkreqN  35751  pmap0  36346  paddasslem17  36417  ltrnnid  36717  dffltz  38678  ntrneikb  39807  fzdifsuc2  41007  limclr  41368  liminflbuz2  41528  fourierdlem42  41866  fourierdlem76  41899  sge0cl  42095  meadjiunlem  42179  oddprmne2  43249  mndpsuppss  43786  islininds2  43907  line2ylem  44107  line2xlem  44109  itsclc0xyqsol  44124  2itscp  44137