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:  notbid  307  con2bi  342  con1bii  345  imor  427  iman  439  dfbi3OLD  1019  ifpn  1042  alex  1793  nfnbi  1821  necon1abid  2861  necon4abid  2863  necon2abid  2865  necon2bbid  2866  necon1abii  2871  dfral2  3023  ralnex2  3074  ralnex3  3075  dfss6  3626  elsymdifxor  3883  falseral0  4114  difsnpss  4370  xpimasn  5614  2mpt20  6924  bropfvvvv  7302  zfregs2  8647  nqereu  9789  ssnn0fi  12824  zeo4  15109  sumodd  15158  ncoprmlnprm  15483  numedglnl  26084  ballotlemfc0  30682  ballotlemfcc  30683  bnj1143  30987  bnj1304  31016  bnj1189  31203  wl-nfnbi  33444  tsim1  34067  tsna1  34081  ecinn0  34258  ifpxorcor  38138  ifpnot23b  38144  ifpnot23c  38146  ifpnot23d  38147  iunrelexp0  38311  con5VD  39450  sineq0ALT  39487  jcn  39519  nepnfltpnf  39871  nemnftgtmnft  39873  sge0gtfsumgt  40978  atbiffatnnb  41400  islininds2  42598  nnolog2flm1  42709