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 144	. 2 ⊢ (𝜑 → ¬ ¬ 𝜑)
2		notnotr 132	. 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  jcndOLD  340  con2bi  357  con1bii  360  con2bii  361  iman  405  imor  850  anor  980  ifpnOLD  1070  noranOLD  1528  nororOLD  1530  alex  1827  nfnbi  1856  necon1abid  2989  necon4abid  2991  necon2abid  2993  necon2bbid  2994  necon1abii  2999  dfral2  3164  dfss6  3881  falseral0  4412  difsnpss  4697  xpimasn  6014  2mpo0  7390  bropfvvvv  7792  zfregs2  9208  nqereu  10389  ssnn0fi  13402  swrdnnn0nd  14065  pfxnd0  14097  zeo4  15739  sumodd  15789  ncoprmlnprm  16123  numedglnl  27036  ballotlemfc0  31978  ballotlemfcc  31979  bnj1143  32290  bnj1304  32319  bnj1189  32509  wl-ifp-ncond2  35162  tsim1  35848  tsna1  35862  ecinn0  36047  ifpxorcor  40557  ifpnot23b  40563  ifpnot23c  40565  ifpnot23d  40566  iunrelexp0  40776  expandrex  41373  con5VD  41979  sineq0ALT  42016  nepnfltpnf  42342  nemnftgtmnft  42344  sge0gtfsumgt  43448  atbiffatnnb  43871  ichnreuop  44357  islininds2  45258  nnolog2flm1  45369  line2ylem  45530