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  853  anor  984  alex  1826  necon1abid  2971  necon4abid  2973  necon2abid  2975  necon2bbid  2976  necon1abii  2981  dfral2  3089  dfss6  3953  falseral0  4496  difsnpss  4788  xpimasn  6179  2mpo0  7661  bropfvvvv  8096  zfregs2  9752  nqereu  10948  ssnn0fi  14008  swrdnnn0nd  14679  pfxnd0  14711  zeo4  16362  sumodd  16412  ncoprmlnprm  16752  numedglnl  29128  ballotlemfc0  34530  ballotlemfcc  34531  bnj1143  34826  bnj1304  34855  bnj1189  35045  wl-ifp-ncond2  37488  tsim1  38159  tsna1  38173  ecinn0  38376  aks4d1p7  42101  aks6d1c5  42157  onsupmaxb  43238  ifpxorcor  43475  ifpnot23b  43481  ifpnot23c  43483  ifpnot23d  43484  iunrelexp0  43701  expandrex  44291  con5VD  44899  sineq0ALT  44936  nepnfltpnf  45349  nemnftgtmnft  45351  sge0gtfsumgt  46452  atbiffatnnb  46921  ichnreuop  47466  islininds2  48440  nnolog2flm1  48550  line2ylem  48711