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  2971  necon4abid  2973  necon2abid  2975  necon2bbid  2976  necon1abii  2981  dfral2  3089  dfss6  3912  falseral0OLD  4456  difsnpss  4751  xpimasn  6144  2mpo0  7610  bropfvvvv  8036  zfregs2  9648  nqereu  10846  ssnn0fi  13941  swrdnnn0nd  14613  pfxnd0  14645  zeo4  16301  sumodd  16351  ncoprmlnprm  16692  numedglnl  29230  ballotlemfc0  34656  ballotlemfcc  34657  bnj1143  34951  bnj1304  34980  bnj1189  35170  bj-cbvaew  36957  wl-ifp-ncond2  37798  tsim1  38468  tsna1  38482  ecinn0  38691  aks4d1p7  42539  aks6d1c5  42595  onsupmaxb  43688  ifpxorcor  43924  ifpnot23b  43930  ifpnot23c  43932  ifpnot23d  43933  iunrelexp0  44150  expandrex  44740  con5VD  45347  sineq0ALT  45384  nepnfltpnf  45793  nemnftgtmnft  45795  sge0gtfsumgt  46892  atbiffatnnb  47375  ichnreuop  47947  islininds2  48975  nnolog2flm1  49081  line2ylem  49242