Theorem nne 3020

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

Syntax hints:  ¬ wn 3   ↔ wb 208   = wceq 1537   ≠ wne 3016

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 209  df-ne 3017

This theorem is referenced by:  neirr  3025  necon3bd  3030  necon1d  3038  necon4d  3040  necon3ai  3041  necon4bid  3061  necon1bbii  3065  pm2.61ine  3100  pm2.61dne  3103  ne3anior  3110  sbcne12  4364  raldifsnb  4729  tpprceq3  4737  tppreqb  4738  prneimg  4785  prnebg  4786  xpeq0  6017  xpcan  6033  xpcan2  6034  fndmdifeq0  6814  ftpg  6918  fnnfpeq0  6940  suppimacnv  7841  fnsuppres  7857  ixp0  8495  isfin5-2  9813  zornn0g  9927  nn0n0n1ge2b  11964  fsuppmapnn0fiub0  13362  fsuppmapnn0ub  13364  mptnn0fsupp  13366  mptnn0fsuppr  13368  discr  13602  hashgt12el  13784  hashgt12el2  13785  hashtpg  13844  fprodle  15350  alzdvds  15670  algcvgblem  15921  lcmfunsnlem2lem2  15983  lssne0  19722  dsmm0cl  20884  pmatcollpw2lem  21385  elcls  21681  cmpfi  22016  bwth  22018  1stccnp  22070  dissnlocfin  22137  trfil3  22496  isufil2  22516  bcth3  23934  rrxmvallem  24007  mdegleb  24658  tglowdim1i  26287  tglineintmo  26428  lmieu  26570  uhgrvd00  27316  wlkon2n0  27448  wwlks  27613  rusgrnumwwlks  27753  clwwlkneq0  27807  1to2vfriswmgr  28058  numclwwlk3lem2  28163  frgrregord013  28174  nmlno0lem  28570  lnon0  28575  nmlnop0iALT  29772  atom1d  30130  uniinn0  30302  nfpconfp  30377  funcnv5mpt  30413  xaddeq0  30477  pmtrcnel  30733  fedgmullem2  31026  bnj521  32007  bnj1533  32124  bnj1541  32128  bnj1279  32290  bnj1280  32292  bnj1311  32296  spthcycl  32376  nepss  32948  bj-ismooredr2  34405  nlpineqsn  34692  poimirlem31  34938  poimirlem32  34939  itg2addnclem2  34959  ftc1anc  34990  n0elqs  35598  lfl1  36221  lkreqN  36321  pmap0  36916  paddasslem17  36987  ltrnnid  37287  dffltz  39320  ntrneikb  40493  fzdifsuc2  41626  limclr  41985  liminflbuz2  42145  fourierdlem42  42483  fourierdlem76  42516  sge0cl  42712  meadjiunlem  42796  oddprmne2  43929  mndpsuppss  44468  islininds2  44588  line2ylem  44787  line2xlem  44789  itsclc0xyqsol  44804  2itscp  44817