Theorem nne 2963

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

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

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 2960

This theorem is used by:  neirr  2968  necon3bd  2973  necon1d  2981  necon4d  2983  necon4bid  3004  necon1bbii  3008  pm2.61ine  3042  ne3anior  3053  sbcne12  4376  raldifsnb  4761  tpprceq3  4769  tppreqb  4770  prneimg  4814  prnebg  4816  xpeq0  6169  xpcan  6186  xpcan2  6187  fndmdifeq0  7074  ftpg  7192  fnnfpeq0  7214  suppimacnv  8229  fnsuppres  8246  suppcoss  8262  ixp0  8997  isfin5-2  10508  zornn0g  10622  nn0n0n1ge2b  12715  fsuppmapnn0fiub0  14176  fsuppmapnn0ub  14178  mptnn0fsupp  14180  mptnn0fsuppr  14182  discr  14425  hashgt12el  14608  hashgt12el2  14609  hashtpg  14671  hash3tpde  14679  fprodle  16207  alzdvds  16534  algcvgblem  16796  lcmfunsnlem2lem2  16858  mndpsuppss  19009  lssne0  21277  dsmm0cl  22101  pmatcollpw2lem  23150  elcls  23446  cmpfi  23781  bwth  23783  1stccnp  23836  dissnlocfin  23903  trfil3  24262  isufil2  24282  bcth3  25707  rrxmvallem  25780  mdegleb  26437  tglowdim1i  29021  tglineintmo  29167  symquadprlnglem  29222  lmieu  29346  prlngsymquadlem  29498  uhgrvd00  30172  wlkon2n0  30302  spthcycl  30449  wwlks  30481  rusgrnumwwlks  30623  clwwlkneq0  30677  1to2vfriswmgr  30937  numclwwlk3lem2  31042  frgrregord013  31053  nmlno0lem  31452  lnon0  31457  nmlnop0iALT  32654  atom1d  33012  n0nsnel  33210  uniinn0  33245  nfpconfp  33324  funcnv5mpt  33359  suppiniseg  33376  xaddeq0  33441  pmtrcnel  33749  1arithidom  34173  esplymhp  34311  fedgmullem2  34373  irredminply  34459  zarcls1  34612  bnj1533  35593  bnj1541  35597  bnj1279  35759  bnj1280  35761  bnj1311  35765  nepss  36698  ttcwf2  37528  bj-ismooredr2  38301  nlpineqsn  38599  poimirlem31  38837  poimirlem32  38838  itg2addnclem2  38858  ftc1anc  38887  n0elqs  39530  suceldisj  40016  lfl1  40393  lkreqN  40493  pmap0  41088  paddasslem17  41159  ltrnnid  41459  sticksstones1  43462  frlmnzcoordex  43918  dffltz  43936  dflim5  44592  ntrneikb  45355  fzdifsuc2  46599  limclr  46938  liminflbuz2  47098  fourierdlem42  47432  fourierdlem76  47465  sge0cl  47664  meadjiunlem  47748  smfpimne2  48123  chnerlem1  48165  n0nsn2el  48368  oddprmne2  49086  usgrexmpl2trifr  49408  islininds2  49927  line2ylem  50194  line2xlem  50196  itsclc0xyqsol  50211  2itscp  50224  dmrnxp  50279  fdomne0  50292  oppcendc  50463  veroquaddetzerod  51414