Theorem nne 2929

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  neirr  2934  necon3bd  2939  necon1d  2947  necon4d  2949  necon4bid  2970  necon1bbii  2974  pm2.61ine  3008  ne3anior  3019  sbcne12  4366  raldifsnb  4747  tpprceq3  4755  tppreqb  4756  prneimg  4805  prnebg  4807  xpeq0  6109  xpcan  6125  xpcan2  6126  fndmdifeq0  6978  ftpg  7090  fnnfpeq0  7114  suppimacnv  8107  fnsuppres  8124  suppcoss  8140  ixp0  8858  isfin5-2  10285  zornn0g  10399  nn0n0n1ge2b  12453  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  18639  lssne0  20854  dsmm0cl  21647  pmatcollpw2lem  22662  elcls  22958  cmpfi  23293  bwth  23295  1stccnp  23347  dissnlocfin  23414  trfil3  23773  isufil2  23793  bcth3  25229  rrxmvallem  25302  mdegleb  25967  tglowdim1i  28446  tglineintmo  28587  lmieu  28729  uhgrvd00  29480  wlkon2n0  29610  wwlks  29780  rusgrnumwwlks  29919  clwwlkneq0  29973  1to2vfriswmgr  30223  numclwwlk3lem2  30328  frgrregord013  30339  nmlno0lem  30737  lnon0  30742  nmlnop0iALT  31939  atom1d  32297  n0nsnel  32459  uniinn0  32494  nfpconfp  32575  funcnv5mpt  32611  suppiniseg  32628  xaddeq0  32696  pmtrcnel  33031  1arithidom  33474  fedgmullem2  33597  irredminply  33683  zarcls1  33836  bnj1533  34819  bnj1541  34823  bnj1279  34985  bnj1280  34987  bnj1311  34991  spthcycl  35102  nepss  35691  bj-ismooredr2  37084  nlpineqsn  37382  poimirlem31  37631  poimirlem32  37632  itg2addnclem2  37652  ftc1anc  37681  n0elqs  38300  lfl1  39049  lkreqN  39149  pmap0  39744  paddasslem17  39815  ltrnnid  40115  sticksstones1  42119  dffltz  42607  dflim5  43302  ntrneikb  44067  fzdifsuc2  45292  limclr  45636  liminflbuz2  45796  fourierdlem42  46130  fourierdlem76  46163  sge0cl  46362  meadjiunlem  46446  smfpimne2  46821  n0nsn2el  47009  oddprmne2  47699  usgrexmpl2trifr  48021  islininds2  48469  line2ylem  48736  line2xlem  48738  itsclc0xyqsol  48753  2itscp  48766  dmrnxp  48821  fdomne0  48834  oppcendc  49003