Theorem notnotb 318

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 143	. 2 ⊢ (𝜑 → ¬ ¬ 𝜑)
2		notnotr 131	. 2 ⊢ (¬ ¬ 𝜑 → 𝜑)
3	1, 2	impbii 212	1 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 209

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 210

This theorem is referenced by:  notbid  321  con2bi  356  con1bii  359  con2bii  360  iman  406  imor  866  anor  998  alex  1853  necon1abid  3002  necon4abid  3004  necon2abid  3006  necon2bbid  3007  necon1abii  3012  dfral2  3122  dfss6  3935  falseral0OLD  4481  difsnpss  4779  xpimasn  6184  2mpo0  7660  bropfvvvv  8087  zfregs2  9702  nqereu  10914  ssnn0fi  14021  swrdnnn0nd  14694  pfxnd0  14726  zeo4  16396  sumodd  16446  ncoprmlnprm  16787  numedglnl  29435  ballotlemfc0  34828  ballotlemfcc  34829  bnj1143  35123  bnj1304  35152  bnj1189  35342  bj-cbvaew  37189  wl-ifp-ncond2  38033  tsim1  38703  tsna1  38717  ecinn0  38926  aks4d1p7  42774  aks6d1c5  42830  onsupmaxb  43892  ifpxorcor  44128  ifpnot23b  44134  ifpnot23c  44136  ifpnot23d  44137  iunrelexp0  44354  expandrex  44928  con5VD  45534  sineq0ALT  45571  nepnfltpnf  45984  nemnftgtmnft  45986  sge0gtfsumgt  47083  atbiffatnnb  47572  ichnreuop  48144  islininds2  49183  nnolog2flm1  49289  line2ylem  49450