Theorem nne 2786

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 2782	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2	1	con2bii 346	. 2 ⊢ (𝐴 = 𝐵 ↔ ¬ 𝐴 ≠ 𝐵)
3	2	bicomi 213	1 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)

Syntax hints:  ¬ wn 3   ↔ wb 195   = wceq 1475   ≠ wne 2780

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 196  df-ne 2782

This theorem is referenced by:  neirr  2791  necon3bd  2796  necon1d  2804  necon4d  2806  necon3ai  2807  necon4bid  2827  necon1bbii  2831  pm2.61ine  2865  pm2.61dne  2868  ne3anior  2875  sbcne12  3938  raldifsnb  4266  tpprceq3  4276  tppreqb  4277  prneimg  4328  prnebg  4329  xpeq0  5473  xpcan  5489  xpcan2  5490  funtpgOLD  5857  fndmdifeq0  6231  ftpg  6328  fnnfpeq0  6349  suppimacnv  7193  fnsuppres  7209  ixp0  7827  isfin5-2  9096  zornn0g  9210  nn0n0n1ge2b  11236  fsuppmapnn0fiub0  12655  fsuppmapnn0ub  12657  mptnn0fsupp  12659  mptnn0fsuppr  12661  discr  12863  hashgt12el  13070  hashgt12el2  13071  hashtpg  13121  fprodle  14566  alzdvds  14880  algcvgblem  15128  lcmfunsnlem2lem2  15190  lssne0  18772  dsmm0cl  19903  pmatcollpw2lem  20401  elcls  20687  cmpfi  21021  bwth  21023  1stccnp  21075  dissnlocfin  21142  trfil3  21502  isufil2  21522  bcth3  22936  rrxmvallem  22995  mdegleb  23628  tglowdim1i  25196  tglineintmo  25337  lmieu  25476  usgrasscusgra  26011  2pthlem2  26126  usgrcyclnl1  26168  rusgranumwlks  26483  1to2vfriswmgra  26533  numclwwlk3lem  26635  frgraregord013  26645  nmlno0lem  27032  lnon0  27037  nmlnop0iALT  28238  atom1d  28596  uniinn0  28749  funcnv5mpt  28852  xaddeq0  28907  bnj521  30059  bnj1533  30176  bnj1541  30180  bnj1279  30340  bnj1280  30342  bnj1311  30346  nepss  30854  poimirlem31  32610  poimirlem32  32611  itg2addnclem2  32632  ftc1anc  32663  lfl1  33375  lkreqN  33475  pmap0  34069  paddasslem17  34140  ltrnnid  34440  ntrneikb  37412  fzdifsuc2  38466  limclr  38722  fourierdlem42  39042  fourierdlem76  39075  sge0cl  39274  meadjiunlem  39358  oddprmne2  40162  uvtxa01vtx  40624  uhgrvd00  40750  wlkOn2n0  40874  wwlks  41038  rusgrnumwwlks  41177  1to2vfriswmgr  41449  av-numclwwlk3lem  41538  av-frgraregord013  41549  mndpsuppss  41946  islininds2  42067