Theorem notnotb 303

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 135	. 2 ⊢ (𝜑 → ¬ ¬ 𝜑)
2		notnotr 124	. 2 ⊢ (¬ ¬ 𝜑 → 𝜑)
3	1, 2	impbii 198	1 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 195

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 196

This theorem is referenced by:  notnotdOLD  304  notbid  307  con2bi  342  con1bii  345  imor  427  iman  439  dfbi3  933  ifpn  1016  alex  1743  necon1abid  2820  necon4abid  2822  necon2abid  2824  necon2bbid  2825  necon1abii  2830  dfral2  2977  ralnex2  3027  ralnex3  3028  elsymdifxor  3812  difsnpss  4279  xpimasn  5498  2mpt20  6780  bropfvvvv  7144  zfregs2  8492  nqereu  9630  ssnn0fi  12646  zeo4  14900  sumodd  14949  ncoprmlnprm  15274  wlkcpr  26057  vdn0frgrav2  26550  vdgn0frgrav2  26551  ballotlemfc0  29881  ballotlemfcc  29882  bnj1143  30115  bnj1304  30144  bnj1189  30331  bj-nfn  31795  wl-nfnbi  32493  tsim1  33107  tsna1  33121  ifpxorcor  36840  ifpnot23b  36846  ifpnot23c  36848  ifpnot23d  36849  iunrelexp0  37013  dfss6  37082  con5VD  38158  sineq0ALT  38195  jcn  38228  nepnfltpnf  38499  nemnftgtmnft  38501  sge0gtfsumgt  39336  atbiffatnnb  39728  falseral0  40308  islininds2  42067  nnolog2flm1  42182