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  2963  necon4abid  2965  necon2abid  2967  necon2bbid  2968  necon1abii  2973  dfral2  3080  dfss6  3925  falseral0  4467  difsnpss  4758  xpimasn  6134  2mpo0  7598  bropfvvvv  8025  zfregs2  9629  nqereu  10823  ssnn0fi  13892  swrdnnn0nd  14563  pfxnd0  14595  zeo4  16249  sumodd  16299  ncoprmlnprm  16639  numedglnl  29089  ballotlemfc0  34467  ballotlemfcc  34468  bnj1143  34763  bnj1304  34792  bnj1189  34982  wl-ifp-ncond2  37449  tsim1  38120  tsna1  38134  ecinn0  38331  aks4d1p7  42066  aks6d1c5  42122  onsupmaxb  43222  ifpxorcor  43459  ifpnot23b  43465  ifpnot23c  43467  ifpnot23d  43468  iunrelexp0  43685  expandrex  44275  con5VD  44883  sineq0ALT  44920  nepnfltpnf  45332  nemnftgtmnft  45334  sge0gtfsumgt  46434  atbiffatnnb  46906  ichnreuop  47466  islininds2  48479  nnolog2flm1  48585  line2ylem  48746