Theorem nne 2798

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 2795	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2	1	con2bii 347	. 2 ⊢ (𝐴 = 𝐵 ↔ ¬ 𝐴 ≠ 𝐵)
3	2	bicomi 214	1 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)

Syntax hints:  ¬ wn 3   ↔ wb 196   = wceq 1483   ≠ wne 2794

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 197  df-ne 2795

This theorem is referenced by:  neirr  2803  necon3bd  2808  necon1d  2816  necon4d  2818  necon3ai  2819  necon4bid  2839  necon1bbii  2843  pm2.61ine  2877  pm2.61dne  2880  ne3anior  2887  sbcne12  3986  raldifsnb  4325  tpprceq3  4335  tppreqb  4336  prneimg  4388  prnebg  4389  xpeq0  5554  xpcan  5570  xpcan2  5571  funtpgOLD  5943  fndmdifeq0  6323  ftpg  6423  fnnfpeq0  6444  suppimacnv  7306  fnsuppres  7322  ixp0  7941  isfin5-2  9213  zornn0g  9327  nn0n0n1ge2b  11359  fsuppmapnn0fiub0  12793  fsuppmapnn0ub  12795  mptnn0fsupp  12797  mptnn0fsuppr  12799  discr  13001  hashgt12el  13210  hashgt12el2  13211  hashtpg  13267  fprodle  14727  alzdvds  15042  algcvgblem  15290  lcmfunsnlem2lem2  15352  lssne0  18951  dsmm0cl  20084  pmatcollpw2lem  20582  elcls  20877  cmpfi  21211  bwth  21213  1stccnp  21265  dissnlocfin  21332  trfil3  21692  isufil2  21712  bcth3  23128  rrxmvallem  23187  mdegleb  23824  tglowdim1i  25396  tglineintmo  25537  lmieu  25676  uvtxa01vtx  26298  uhgrvd00  26430  wlkon2n0  26562  wwlks  26727  rusgrnumwwlks  26869  1to2vfriswmgr  27143  numclwwlk3lem  27241  frgrregord013  27253  nmlno0lem  27648  lnon0  27653  nmlnop0iALT  28854  atom1d  29212  uniinn0  29366  funcnv5mpt  29469  xaddeq0  29518  bnj521  30805  bnj1533  30922  bnj1541  30926  bnj1279  31086  bnj1280  31088  bnj1311  31092  nepss  31599  poimirlem31  33440  poimirlem32  33441  itg2addnclem2  33462  ftc1anc  33493  n0elqs  34098  lfl1  34357  lkreqN  34457  pmap0  35051  paddasslem17  35122  ltrnnid  35422  ntrneikb  38392  fzdifsuc2  39525  limclr  39887  fourierdlem42  40366  fourierdlem76  40399  sge0cl  40598  meadjiunlem  40682  oddprmne2  41624  mndpsuppss  42152  islininds2  42273