Theorem nne 2946

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

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1539   ≠ wne 2942

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 206  df-ne 2943

This theorem is referenced by:  neirr  2951  necon3bd  2956  necon1d  2964  necon4d  2966  necon3aiOLD  2968  necon4bid  2988  necon1bbii  2992  pm2.61ine  3027  ne3anior  3037  sbcne12  4343  raldifsnb  4726  tpprceq3  4734  tppreqb  4735  prneimg  4782  prnebg  4783  xpeq0  6052  xpcan  6068  xpcan2  6069  fndmdifeq0  6903  ftpg  7010  fnnfpeq0  7032  suppimacnv  7961  fnsuppres  7978  suppcoss  7994  ixp0  8677  isfin5-2  10078  zornn0g  10192  nn0n0n1ge2b  12231  fsuppmapnn0fiub0  13641  fsuppmapnn0ub  13643  mptnn0fsupp  13645  mptnn0fsuppr  13647  discr  13883  hashgt12el  14065  hashgt12el2  14066  hashtpg  14127  fprodle  15634  alzdvds  15957  algcvgblem  16210  lcmfunsnlem2lem2  16272  lssne0  20127  dsmm0cl  20857  pmatcollpw2lem  21834  elcls  22132  cmpfi  22467  bwth  22469  1stccnp  22521  dissnlocfin  22588  trfil3  22947  isufil2  22967  bcth3  24400  rrxmvallem  24473  mdegleb  25134  tglowdim1i  26766  tglineintmo  26907  lmieu  27049  uhgrvd00  27804  wlkon2n0  27936  wwlks  28101  rusgrnumwwlks  28240  clwwlkneq0  28294  1to2vfriswmgr  28544  numclwwlk3lem2  28649  frgrregord013  28660  nmlno0lem  29056  lnon0  29061  nmlnop0iALT  30258  atom1d  30616  uniinn0  30791  nfpconfp  30868  funcnv5mpt  30907  suppiniseg  30922  xaddeq0  30978  pmtrcnel  31260  fedgmullem2  31613  zarcls1  31721  bnj521  32616  bnj1533  32732  bnj1541  32736  bnj1279  32898  bnj1280  32900  bnj1311  32904  spthcycl  32991  nepss  33564  bj-ismooredr2  35208  nlpineqsn  35506  poimirlem31  35735  poimirlem32  35736  itg2addnclem2  35756  ftc1anc  35785  n0elqs  36388  lfl1  37011  lkreqN  37111  pmap0  37706  paddasslem17  37777  ltrnnid  38077  sticksstones1  40030  dffltz  40387  ntrneikb  41593  fzdifsuc2  42739  limclr  43086  liminflbuz2  43246  fourierdlem42  43580  fourierdlem76  43613  sge0cl  43809  meadjiunlem  43893  oddprmne2  45055  mndpsuppss  45595  islininds2  45713  line2ylem  45985  line2xlem  45987  itsclc0xyqsol  46002  2itscp  46015  fdomne0  46065