Theorem nne 2961

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 2958	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2	1	con2bii 359	. 2 ⊢ (𝐴 = 𝐵 ↔ ¬ 𝐴 ≠ 𝐵)
3	2	bicomi 226	1 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)

Syntax hints:  ¬ wn 3   ↔ wb 208   = wceq 1560   ≠ wne 2957

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 209  df-ne 2958

This theorem is referenced by:  neirr  2966  necon3bd  2971  necon1d  2979  necon4d  2981  necon4bid  3002  necon1bbii  3006  pm2.61ine  3040  ne3anior  3051  sbcne12  4369  raldifsnb  4756  tpprceq3  4764  tppreqb  4765  prneimg  4812  prnebg  4814  xpeq0  6145  xpcan  6162  xpcan2  6163  fndmdifeq0  7025  ftpg  7139  fnnfpeq0  7162  suppimacnv  8154  fnsuppres  8171  suppcoss  8187  ixp0  8913  isfin5-2  10348  zornn0g  10462  nn0n0n1ge2b  12550  fsuppmapnn0fiub0  14006  fsuppmapnn0ub  14008  mptnn0fsupp  14010  mptnn0fsuppr  14012  discr  14253  hashgt12el  14435  hashgt12el2  14436  hashtpg  14498  hash3tpde  14506  fprodle  16026  alzdvds  16354  algcvgblem  16611  lcmfunsnlem2lem2  16673  mndpsuppss  18799  lssne0  21015  dsmm0cl  21789  pmatcollpw2lem  22834  elcls  23130  cmpfi  23465  bwth  23467  1stccnp  23519  dissnlocfin  23586  trfil3  23945  isufil2  23965  bcth3  25390  rrxmvallem  25463  mdegleb  26121  tglowdim1i  28667  tglineintmo  28808  lmieu  28954  uhgrvd00  29732  wlkon2n0  29862  wwlks  30032  rusgrnumwwlks  30174  clwwlkneq0  30228  1to2vfriswmgr  30478  numclwwlk3lem2  30583  frgrregord013  30594  nmlno0lem  30993  lnon0  30998  nmlnop0iALT  32195  atom1d  32553  n0nsnel  32711  uniinn0  32747  nfpconfp  32831  funcnv5mpt  32866  suppiniseg  32885  xaddeq0  32952  pmtrcnel  33266  1arithidom  33730  esplymhp  33862  fedgmullem2  33924  irredminply  34010  zarcls1  34163  bnj1533  35144  bnj1541  35148  bnj1279  35310  bnj1280  35312  bnj1311  35316  spthcycl  35476  nepss  36065  ttcwf2  36882  bj-ismooredr2  37597  nlpineqsn  37899  poimirlem31  38147  poimirlem32  38148  itg2addnclem2  38168  ftc1anc  38197  n0elqs  38828  suceldisj  39314  lfl1  39691  lkreqN  39791  pmap0  40386  paddasslem17  40457  ltrnnid  40757  sticksstones1  42760  dffltz  43213  dflim5  43903  ntrneikb  44667  fzdifsuc2  45886  limclr  46226  liminflbuz2  46386  fourierdlem42  46720  fourierdlem76  46753  sge0cl  46952  meadjiunlem  47036  smfpimne2  47411  chnerlem1  47455  n0nsn2el  47616  oddprmne2  48334  usgrexmpl2trifr  48656  islininds2  49103  line2ylem  49370  line2xlem  49372  itsclc0xyqsol  49387  2itscp  49400  dmrnxp  49455  fdomne0  49468  oppcendc  49636