Theorem nne 2948

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

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

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 2945

This theorem is referenced by:  neirr  2953  necon3bd  2958  necon1d  2966  necon4d  2968  necon3aiOLD  2970  necon4bid  2990  necon1bbii  2994  pm2.61ine  3029  ne3anior  3039  sbcne12  4347  raldifsnb  4730  tpprceq3  4738  tppreqb  4739  prneimg  4786  prnebg  4787  xpeq0  6068  xpcan  6084  xpcan2  6085  fndmdifeq0  6930  ftpg  7037  fnnfpeq0  7059  suppimacnv  7999  fnsuppres  8016  suppcoss  8032  ixp0  8728  isfin5-2  10156  zornn0g  10270  nn0n0n1ge2b  12310  fsuppmapnn0fiub0  13722  fsuppmapnn0ub  13724  mptnn0fsupp  13726  mptnn0fsuppr  13728  discr  13964  hashgt12el  14146  hashgt12el2  14147  hashtpg  14208  fprodle  15715  alzdvds  16038  algcvgblem  16291  lcmfunsnlem2lem2  16353  lssne0  20221  dsmm0cl  20956  pmatcollpw2lem  21935  elcls  22233  cmpfi  22568  bwth  22570  1stccnp  22622  dissnlocfin  22689  trfil3  23048  isufil2  23068  bcth3  24504  rrxmvallem  24577  mdegleb  25238  tglowdim1i  26871  tglineintmo  27012  lmieu  27154  uhgrvd00  27910  wlkon2n0  28043  wwlks  28209  rusgrnumwwlks  28348  clwwlkneq0  28402  1to2vfriswmgr  28652  numclwwlk3lem2  28757  frgrregord013  28768  nmlno0lem  29164  lnon0  29169  nmlnop0iALT  30366  atom1d  30724  uniinn0  30899  nfpconfp  30976  funcnv5mpt  31014  suppiniseg  31029  xaddeq0  31085  pmtrcnel  31367  fedgmullem2  31720  zarcls1  31828  bnj521  32725  bnj1533  32841  bnj1541  32845  bnj1279  33007  bnj1280  33009  bnj1311  33013  spthcycl  33100  nepss  33671  bj-ismooredr2  35290  nlpineqsn  35588  poimirlem31  35817  poimirlem32  35818  itg2addnclem2  35838  ftc1anc  35867  n0elqs  36468  lfl1  37091  lkreqN  37191  pmap0  37786  paddasslem17  37857  ltrnnid  38157  sticksstones1  40109  dffltz  40478  ntrneikb  41711  fzdifsuc2  42856  limclr  43203  liminflbuz2  43363  fourierdlem42  43697  fourierdlem76  43730  sge0cl  43926  meadjiunlem  44010  oddprmne2  45178  mndpsuppss  45718  islininds2  45836  line2ylem  46108  line2xlem  46110  itsclc0xyqsol  46125  2itscp  46138  fdomne0  46188