Theorem nne 2951

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

Syntax hints:  ¬ wn 3   ↔ wb 208   = wceq 1550   ≠ wne 2947

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 2948

This theorem is referenced by:  neirr  2956  necon3bd  2961  necon1d  2969  necon4d  2971  necon4bid  2992  necon1bbii  2996  pm2.61ine  3030  ne3anior  3041  sbcne12  4359  raldifsnb  4746  tpprceq3  4754  tppreqb  4755  prneimg  4802  prnebg  4804  xpeq0  6131  xpcan  6147  xpcan2  6148  fndmdifeq0  7010  ftpg  7124  fnnfpeq0  7147  suppimacnv  8138  fnsuppres  8155  suppcoss  8171  ixp0  8898  isfin5-2  10334  zornn0g  10448  nn0n0n1ge2b  12536  fsuppmapnn0fiub0  13992  fsuppmapnn0ub  13994  mptnn0fsupp  13996  mptnn0fsuppr  13998  discr  14239  hashgt12el  14421  hashgt12el2  14422  hashtpg  14484  hash3tpde  14492  fprodle  15998  alzdvds  16326  algcvgblem  16583  lcmfunsnlem2lem2  16645  mndpsuppss  18771  lssne0  20987  dsmm0cl  21761  pmatcollpw2lem  22806  elcls  23102  cmpfi  23437  bwth  23439  1stccnp  23491  dissnlocfin  23558  trfil3  23917  isufil2  23937  bcth3  25362  rrxmvallem  25435  mdegleb  26093  tglowdim1i  28636  tglineintmo  28777  lmieu  28919  uhgrvd00  29670  wlkon2n0  29800  wwlks  29970  rusgrnumwwlks  30112  clwwlkneq0  30166  1to2vfriswmgr  30416  numclwwlk3lem2  30521  frgrregord013  30532  nmlno0lem  30931  lnon0  30936  nmlnop0iALT  32133  atom1d  32491  n0nsnel  32652  uniinn0  32688  nfpconfp  32773  funcnv5mpt  32808  suppiniseg  32827  xaddeq0  32894  pmtrcnel  33219  1arithidom  33677  esplymhp  33809  fedgmullem2  33871  irredminply  33957  zarcls1  34110  bnj1533  35094  bnj1541  35098  bnj1279  35260  bnj1280  35262  bnj1311  35266  spthcycl  35417  nepss  36006  ttcwf2  36823  bj-ismooredr2  37538  nlpineqsn  37840  poimirlem31  38088  poimirlem32  38089  itg2addnclem2  38109  ftc1anc  38138  n0elqs  38769  suceldisj  39255  lfl1  39632  lkreqN  39732  pmap0  40327  paddasslem17  40398  ltrnnid  40698  sticksstones1  42701  dffltz  43154  dflim5  43844  ntrneikb  44608  fzdifsuc2  45827  limclr  46167  liminflbuz2  46327  fourierdlem42  46661  fourierdlem76  46694  sge0cl  46893  meadjiunlem  46977  smfpimne2  47352  chnerlem1  47396  n0nsn2el  47557  oddprmne2  48275  usgrexmpl2trifr  48597  islininds2  49044  line2ylem  49311  line2xlem  49313  itsclc0xyqsol  49328  2itscp  49341  dmrnxp  49396  fdomne0  49409  oppcendc  49577