Theorem notnotb 304

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 136	. 2 ⊢ (𝜑 → ¬ ¬ 𝜑)
2		notnotr 125	. 2 ⊢ (¬ ¬ 𝜑 → 𝜑)
3	1, 2	impbii 199	1 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 196

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 197

This theorem is referenced by:  notnotdOLD  305  notbid  308  con2bi  343  con1bii  346  imor  428  iman  440  dfbi3OLD  995  ifpn  1022  alex  1753  nfnbi  1781  necon1abid  2832  necon4abid  2834  necon2abid  2836  necon2bbid  2837  necon1abii  2842  dfral2  2994  ralnex2  3045  ralnex3  3046  dfss6  3593  elsymdifxor  3850  falseral0  4081  difsnpss  4338  xpimasn  5579  2mpt20  6882  bropfvvvv  7257  zfregs2  8609  nqereu  9751  ssnn0fi  12784  zeo4  15062  sumodd  15111  ncoprmlnprm  15436  numedglnl  26039  ballotlemfc0  30554  ballotlemfcc  30555  bnj1143  30861  bnj1304  30890  bnj1189  31077  wl-nfnbi  33314  tsim1  33937  tsna1  33951  ecinn0  34118  ifpxorcor  37821  ifpnot23b  37827  ifpnot23c  37829  ifpnot23d  37830  iunrelexp0  37994  con5VD  39136  sineq0ALT  39173  jcn  39205  nepnfltpnf  39558  nemnftgtmnft  39560  sge0gtfsumgt  40660  atbiffatnnb  41079  islininds2  42273  nnolog2flm1  42384