Theorem notnotb 315

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 142	. 2 ⊢ (𝜑 → ¬ ¬ 𝜑)
2		notnotr 130	. 2 ⊢ (¬ ¬ 𝜑 → 𝜑)
3	1, 2	impbii 209	1 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206

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 207

This theorem is referenced by:  notbid  318  con2bi  353  con1bii  356  con2bii  357  iman  401  imor  853  anor  984  alex  1827  necon1abid  2966  necon4abid  2968  necon2abid  2970  necon2bbid  2971  necon1abii  2976  dfral2  3083  dfss6  3919  falseral0  4463  difsnpss  4756  xpimasn  6132  2mpo0  7595  bropfvvvv  8022  zfregs2  9623  nqereu  10820  ssnn0fi  13892  swrdnnn0nd  14564  pfxnd0  14596  zeo4  16249  sumodd  16299  ncoprmlnprm  16639  numedglnl  29122  ballotlemfc0  34506  ballotlemfcc  34507  bnj1143  34802  bnj1304  34831  bnj1189  35021  wl-ifp-ncond2  37509  tsim1  38180  tsna1  38194  ecinn0  38395  aks4d1p7  42186  aks6d1c5  42242  onsupmaxb  43342  ifpxorcor  43579  ifpnot23b  43585  ifpnot23c  43587  ifpnot23d  43588  iunrelexp0  43805  expandrex  44395  con5VD  45002  sineq0ALT  45039  nepnfltpnf  45451  nemnftgtmnft  45453  sge0gtfsumgt  46551  atbiffatnnb  47022  ichnreuop  47582  islininds2  48595  nnolog2flm1  48701  line2ylem  48862