Theorem nne 2932

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 2929	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2	1	con2bii 357	. 2 ⊢ (𝐴 = 𝐵 ↔ ¬ 𝐴 ≠ 𝐵)
3	2	bicomi 224	1 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1541   ≠ wne 2928

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 207  df-ne 2929

This theorem is referenced by:  neirr  2937  necon3bd  2942  necon1d  2950  necon4d  2952  necon4bid  2973  necon1bbii  2977  pm2.61ine  3011  ne3anior  3022  sbcne12  4362  raldifsnb  4745  tpprceq3  4753  tppreqb  4754  prneimg  4803  prnebg  4805  xpeq0  6107  xpcan  6123  xpcan2  6124  fndmdifeq0  6977  ftpg  7089  fnnfpeq0  7112  suppimacnv  8104  fnsuppres  8121  suppcoss  8137  ixp0  8855  isfin5-2  10282  zornn0g  10396  nn0n0n1ge2b  12450  fsuppmapnn0fiub0  13900  fsuppmapnn0ub  13902  mptnn0fsupp  13904  mptnn0fsuppr  13906  discr  14147  hashgt12el  14329  hashgt12el2  14330  hashtpg  14392  hash3tpde  14400  fprodle  15903  alzdvds  16231  algcvgblem  16488  lcmfunsnlem2lem2  16550  mndpsuppss  18673  lssne0  20884  dsmm0cl  21677  pmatcollpw2lem  22692  elcls  22988  cmpfi  23323  bwth  23325  1stccnp  23377  dissnlocfin  23444  trfil3  23803  isufil2  23823  bcth3  25258  rrxmvallem  25331  mdegleb  25996  tglowdim1i  28479  tglineintmo  28620  lmieu  28762  uhgrvd00  29513  wlkon2n0  29643  wwlks  29813  rusgrnumwwlks  29955  clwwlkneq0  30009  1to2vfriswmgr  30259  numclwwlk3lem2  30364  frgrregord013  30375  nmlno0lem  30773  lnon0  30778  nmlnop0iALT  31975  atom1d  32333  n0nsnel  32495  uniinn0  32530  nfpconfp  32614  funcnv5mpt  32650  suppiniseg  32667  xaddeq0  32736  pmtrcnel  33058  1arithidom  33502  esplymhp  33589  fedgmullem2  33643  irredminply  33729  zarcls1  33882  bnj1533  34864  bnj1541  34868  bnj1279  35030  bnj1280  35032  bnj1311  35036  spthcycl  35173  nepss  35762  bj-ismooredr2  37154  nlpineqsn  37452  poimirlem31  37701  poimirlem32  37702  itg2addnclem2  37722  ftc1anc  37751  n0elqs  38374  lfl1  39179  lkreqN  39279  pmap0  39874  paddasslem17  39945  ltrnnid  40245  sticksstones1  42249  dffltz  42737  dflim5  43432  ntrneikb  44197  fzdifsuc2  45421  limclr  45763  liminflbuz2  45923  fourierdlem42  46257  fourierdlem76  46290  sge0cl  46489  meadjiunlem  46573  smfpimne2  46948  chnerlem1  46990  n0nsn2el  47135  oddprmne2  47825  usgrexmpl2trifr  48147  islininds2  48595  line2ylem  48862  line2xlem  48864  itsclc0xyqsol  48879  2itscp  48892  dmrnxp  48947  fdomne0  48960  oppcendc  49129