Theorem nne 2936

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1542   ≠ wne 2932

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 2933

This theorem is referenced by:  neirr  2941  necon3bd  2946  necon1d  2954  necon4d  2956  necon4bid  2977  necon1bbii  2981  pm2.61ine  3015  ne3anior  3026  sbcne12  4355  raldifsnb  4741  tpprceq3  4749  tppreqb  4750  prneimg  4797  prnebg  4799  xpeq0  6124  xpcan  6140  xpcan2  6141  fndmdifeq0  6996  ftpg  7110  fnnfpeq0  7133  suppimacnv  8124  fnsuppres  8141  suppcoss  8157  ixp0  8879  isfin5-2  10313  zornn0g  10427  nn0n0n1ge2b  12506  fsuppmapnn0fiub0  13955  fsuppmapnn0ub  13957  mptnn0fsupp  13959  mptnn0fsuppr  13961  discr  14202  hashgt12el  14384  hashgt12el2  14385  hashtpg  14447  hash3tpde  14455  fprodle  15961  alzdvds  16289  algcvgblem  16546  lcmfunsnlem2lem2  16608  mndpsuppss  18733  lssne0  20946  dsmm0cl  21720  pmatcollpw2lem  22742  elcls  23038  cmpfi  23373  bwth  23375  1stccnp  23427  dissnlocfin  23494  trfil3  23853  isufil2  23873  bcth3  25298  rrxmvallem  25371  mdegleb  26029  tglowdim1i  28569  tglineintmo  28710  lmieu  28852  uhgrvd00  29603  wlkon2n0  29733  wwlks  29903  rusgrnumwwlks  30045  clwwlkneq0  30099  1to2vfriswmgr  30349  numclwwlk3lem2  30454  frgrregord013  30465  nmlno0lem  30864  lnon0  30869  nmlnop0iALT  32066  atom1d  32424  n0nsnel  32585  uniinn0  32620  nfpconfp  32705  funcnv5mpt  32740  suppiniseg  32759  xaddeq0  32826  pmtrcnel  33150  1arithidom  33597  esplymhp  33712  fedgmullem2  33774  irredminply  33860  zarcls1  34013  bnj1533  34994  bnj1541  34998  bnj1279  35160  bnj1280  35162  bnj1311  35166  spthcycl  35311  nepss  35900  ttcwf2  36707  bj-ismooredr2  37422  nlpineqsn  37724  poimirlem31  37972  poimirlem32  37973  itg2addnclem2  37993  ftc1anc  38022  n0elqs  38653  suceldisj  39139  lfl1  39516  lkreqN  39616  pmap0  40211  paddasslem17  40282  ltrnnid  40582  sticksstones1  42585  dffltz  43067  dflim5  43757  ntrneikb  44521  fzdifsuc2  45743  limclr  46083  liminflbuz2  46243  fourierdlem42  46577  fourierdlem76  46610  sge0cl  46809  meadjiunlem  46893  smfpimne2  47268  chnerlem1  47312  n0nsn2el  47473  oddprmne2  48191  usgrexmpl2trifr  48513  islininds2  48960  line2ylem  49227  line2xlem  49229  itsclc0xyqsol  49244  2itscp  49257  dmrnxp  49312  fdomne0  49325  oppcendc  49493