Theorem nne 2943

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1539   ≠ wne 2939

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 2940

This theorem is referenced by:  neirr  2948  necon3bd  2953  necon1d  2961  necon4d  2963  necon3aiOLD  2965  necon4bid  2985  necon1bbii  2989  pm2.61ine  3024  ne3anior  3035  sbcne12  4414  raldifsnb  4795  tpprceq3  4803  tppreqb  4804  prneimg  4853  prnebg  4855  xpeq0  6179  xpcan  6195  xpcan2  6196  fndmdifeq0  7063  ftpg  7175  fnnfpeq0  7199  suppimacnv  8200  fnsuppres  8217  suppcoss  8233  ixp0  8972  isfin5-2  10432  zornn0g  10546  nn0n0n1ge2b  12597  fsuppmapnn0fiub0  14035  fsuppmapnn0ub  14037  mptnn0fsupp  14039  mptnn0fsuppr  14041  discr  14280  hashgt12el  14462  hashgt12el2  14463  hashtpg  14525  hash3tpde  14533  fprodle  16033  alzdvds  16358  algcvgblem  16615  lcmfunsnlem2lem2  16677  mndpsuppss  18779  lssne0  20950  dsmm0cl  21761  pmatcollpw2lem  22784  elcls  23082  cmpfi  23417  bwth  23419  1stccnp  23471  dissnlocfin  23538  trfil3  23897  isufil2  23917  bcth3  25366  rrxmvallem  25439  mdegleb  26104  tglowdim1i  28510  tglineintmo  28651  lmieu  28793  uhgrvd00  29553  wlkon2n0  29685  wwlks  29856  rusgrnumwwlks  29995  clwwlkneq0  30049  1to2vfriswmgr  30299  numclwwlk3lem2  30404  frgrregord013  30415  nmlno0lem  30813  lnon0  30818  nmlnop0iALT  32015  atom1d  32373  n0nsnel  32535  uniinn0  32564  nfpconfp  32643  funcnv5mpt  32679  suppiniseg  32696  xaddeq0  32758  pmtrcnel  33110  1arithidom  33566  fedgmullem2  33682  irredminply  33758  zarcls1  33869  bnj1533  34867  bnj1541  34871  bnj1279  35033  bnj1280  35035  bnj1311  35039  spthcycl  35135  nepss  35719  bj-ismooredr2  37112  nlpineqsn  37410  poimirlem31  37659  poimirlem32  37660  itg2addnclem2  37680  ftc1anc  37709  n0elqs  38328  lfl1  39072  lkreqN  39172  pmap0  39768  paddasslem17  39839  ltrnnid  40139  sticksstones1  42148  dffltz  42649  dflim5  43347  ntrneikb  44112  fzdifsuc2  45327  limclr  45675  liminflbuz2  45835  fourierdlem42  46169  fourierdlem76  46202  sge0cl  46401  meadjiunlem  46485  smfpimne2  46860  n0nsn2el  47042  oddprmne2  47707  usgrexmpl2trifr  48001  islininds2  48406  line2ylem  48677  line2xlem  48679  itsclc0xyqsol  48694  2itscp  48707  fdomne0  48764  oppcendc  48921