Theorem nne 2964

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 2961	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2	1	con2bii 360	. 2 ⊢ (𝐴 = 𝐵 ↔ ¬ 𝐴 ≠ 𝐵)
3	2	bicomi 227	1 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   = wceq 1570   ≠ wne 2960

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2961

This theorem is used by:  neirr  2969  necon3bd  2974  necon1d  2982  necon4d  2984  necon4bid  3005  necon1bbii  3009  pm2.61ine  3043  ne3anior  3054  sbcne12  4380  raldifsnb  4766  tpprceq3  4774  tppreqb  4775  prneimg  4821  prnebg  4823  xpeq0  6159  xpcan  6176  xpcan2  6177  fndmdifeq0  7043  ftpg  7159  fnnfpeq0  7182  suppimacnv  8176  fnsuppres  8193  suppcoss  8209  ixp0  8935  isfin5-2  10390  zornn0g  10504  nn0n0n1ge2b  12588  fsuppmapnn0fiub0  14047  fsuppmapnn0ub  14049  mptnn0fsupp  14051  mptnn0fsuppr  14053  discr  14294  hashgt12el  14477  hashgt12el2  14478  hashtpg  14540  hash3tpde  14548  fprodle  16073  alzdvds  16400  algcvgblem  16657  lcmfunsnlem2lem2  16719  mndpsuppss  18860  lssne0  21122  dsmm0cl  21940  pmatcollpw2lem  22984  elcls  23280  cmpfi  23615  bwth  23617  1stccnp  23670  dissnlocfin  23737  trfil3  24096  isufil2  24116  bcth3  25541  rrxmvallem  25614  mdegleb  26272  tglowdim1i  28821  tglineintmo  28966  symquadprlnglem  29021  lmieu  29144  prlngsymquadlem  29268  uhgrvd00  29942  wlkon2n0  30072  spthcycl  30219  wwlks  30251  rusgrnumwwlks  30393  clwwlkneq0  30447  1to2vfriswmgr  30701  numclwwlk3lem2  30806  frgrregord013  30817  nmlno0lem  31216  lnon0  31221  nmlnop0iALT  32418  atom1d  32776  n0nsnel  32932  uniinn0  32968  nfpconfp  33048  funcnv5mpt  33083  suppiniseg  33102  xaddeq0  33168  pmtrcnel  33473  1arithidom  33891  esplymhp  34022  fedgmullem2  34084  irredminply  34170  zarcls1  34323  bnj1533  35305  bnj1541  35309  bnj1279  35471  bnj1280  35473  bnj1311  35477  nepss  36247  ttcwf2  37093  bj-ismooredr2  37809  nlpineqsn  38111  poimirlem31  38359  poimirlem32  38360  itg2addnclem2  38380  ftc1anc  38409  n0elqs  39039  suceldisj  39525  lfl1  39902  lkreqN  40002  pmap0  40597  paddasslem17  40668  ltrnnid  40968  sticksstones1  42971  dffltz  43424  dflim5  44114  ntrneikb  44878  fzdifsuc2  46087  limclr  46427  liminflbuz2  46587  fourierdlem42  46921  fourierdlem76  46954  sge0cl  47153  meadjiunlem  47237  smfpimne2  47612  chnerlem1  47656  n0nsn2el  47820  oddprmne2  48538  usgrexmpl2trifr  48860  islininds2  49321  line2ylem  49588  line2xlem  49590  itsclc0xyqsol  49605  2itscp  49618  dmrnxp  49672  fdomne0  49685  oppcendc  49853