Theorem notnotb 315

Description: Double negation. Theorem *4.13 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-1993.)

Assertion

Ref	Expression
notnotb	⊢ (𝜑 ↔ ¬ ¬ 𝜑)

Proof of Theorem notnotb

Step	Hyp	Ref	Expression
1		notnot 142	. 2 ⊢ (𝜑 → ¬ ¬ 𝜑)
2		notnotr 130	. 2 ⊢ (¬ ¬ 𝜑 → 𝜑)
3	1, 2	impbii 209	1 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206

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

This theorem is referenced by:  notbid  318  con2bi  353  con1bii  356  con2bii  357  iman  401  imor  854  anor  985  alex  1828  necon1abid  2970  necon4abid  2972  necon2abid  2974  necon2bbid  2975  necon1abii  2980  dfral2  3088  dfss6  3911  falseral0OLD  4455  difsnpss  4752  xpimasn  6149  2mpo0  7616  bropfvvvv  8042  zfregs2  9654  nqereu  10852  ssnn0fi  13947  swrdnnn0nd  14619  pfxnd0  14651  zeo4  16307  sumodd  16357  ncoprmlnprm  16698  numedglnl  29213  ballotlemfc0  34637  ballotlemfcc  34638  bnj1143  34932  bnj1304  34961  bnj1189  35151  bj-cbvaew  36938  wl-ifp-ncond2  37781  tsim1  38451  tsna1  38465  ecinn0  38674  aks4d1p7  42522  aks6d1c5  42578  onsupmaxb  43667  ifpxorcor  43903  ifpnot23b  43909  ifpnot23c  43911  ifpnot23d  43912  iunrelexp0  44129  expandrex  44719  con5VD  45326  sineq0ALT  45363  nepnfltpnf  45772  nemnftgtmnft  45774  sge0gtfsumgt  46871  atbiffatnnb  47360  ichnreuop  47932  islininds2  48960  nnolog2flm1  49066  line2ylem  49227