Theorem nne 2950

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1537   ≠ wne 2946

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 2947

This theorem is referenced by:  neirr  2955  necon3bd  2960  necon1d  2968  necon4d  2970  necon3aiOLD  2972  necon4bid  2992  necon1bbii  2996  pm2.61ine  3031  ne3anior  3042  sbcne12  4438  raldifsnb  4821  tpprceq3  4829  tppreqb  4830  prneimg  4879  prnebg  4880  xpeq0  6191  xpcan  6207  xpcan2  6208  fndmdifeq0  7077  ftpg  7190  fnnfpeq0  7212  suppimacnv  8215  fnsuppres  8232  suppcoss  8248  ixp0  8989  isfin5-2  10460  zornn0g  10574  nn0n0n1ge2b  12621  fsuppmapnn0fiub0  14044  fsuppmapnn0ub  14046  mptnn0fsupp  14048  mptnn0fsuppr  14050  discr  14289  hashgt12el  14471  hashgt12el2  14472  hashtpg  14534  hash3tpde  14542  fprodle  16044  alzdvds  16368  algcvgblem  16624  lcmfunsnlem2lem2  16686  lssne0  20972  dsmm0cl  21783  pmatcollpw2lem  22804  elcls  23102  cmpfi  23437  bwth  23439  1stccnp  23491  dissnlocfin  23558  trfil3  23917  isufil2  23937  bcth3  25384  rrxmvallem  25457  mdegleb  26123  tglowdim1i  28527  tglineintmo  28668  lmieu  28810  uhgrvd00  29570  wlkon2n0  29702  wwlks  29868  rusgrnumwwlks  30007  clwwlkneq0  30061  1to2vfriswmgr  30311  numclwwlk3lem2  30416  frgrregord013  30427  nmlno0lem  30825  lnon0  30830  nmlnop0iALT  32027  atom1d  32385  n0nsnel  32544  uniinn0  32573  nfpconfp  32651  funcnv5mpt  32686  suppiniseg  32698  xaddeq0  32760  pmtrcnel  33082  1arithidom  33530  fedgmullem2  33643  irredminply  33707  zarcls1  33815  bnj1533  34828  bnj1541  34832  bnj1279  34994  bnj1280  34996  bnj1311  35000  spthcycl  35097  nepss  35680  bj-ismooredr2  37076  nlpineqsn  37374  poimirlem31  37611  poimirlem32  37612  itg2addnclem2  37632  ftc1anc  37661  n0elqs  38282  lfl1  39026  lkreqN  39126  pmap0  39722  paddasslem17  39793  ltrnnid  40093  sticksstones1  42103  dffltz  42589  dflim5  43291  ntrneikb  44056  fzdifsuc2  45225  limclr  45576  liminflbuz2  45736  fourierdlem42  46070  fourierdlem76  46103  sge0cl  46302  meadjiunlem  46386  smfpimne2  46761  n0nsn2el  46940  oddprmne2  47589  usgrexmpl2trifr  47852  mndpsuppss  48096  islininds2  48213  line2ylem  48485  line2xlem  48487  itsclc0xyqsol  48502  2itscp  48515  fdomne0  48563