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 143	. 2 ⊢ (𝜑 → ¬ ¬ 𝜑)
2		notnotr 131	. 2 ⊢ (¬ ¬ 𝜑 → 𝜑)
3	1, 2	impbii 212	1 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  notbid  321  con2bi  356  con1bii  359  con2bii  360  iman  407  imor  867  anor  998  alex  1858  necon1abid  2997  necon4abid  2999  necon2abid  3001  necon2bbid  3002  necon1abii  3007  dfral2  3117  dfss6  3903  falseral0OLD  4474  difsnpss  4770  xpimasn  6183  2mpo0  7680  bropfvvvv  8114  zfregs2  9747  nqereu  11027  ssnn0fi  14141  swrdnnn0nd  14820  pfxnd0  14852  zeo4  16523  sumodd  16573  ncoprmlnprm  16919  numedglnl  29737  ballotlemfc0  35181  ballotlemfcc  35182  bnj1143  35476  bnj1304  35505  bnj1189  35695  bj-cbvaew  37673  wl-ifp-ncond2  38531  tsim1  39205  tsna1  39219  ecinn0  39428  aks4d1p7  43276  aks6d1c5  43332  onsupmaxb  44384  ifpxorcor  44620  ifpnot23b  44626  ifpnot23c  44628  ifpnot23d  44629  iunrelexp0  44845  expandrex  45419  con5VD  46024  sineq0ALT  46061  nepnfltpnf  46496  nemnftgtmnft  46498  sge0gtfsumgt  47595  atbiffatnnb  48124  ichnreuop  48696  islininds2  49738  nnolog2flm1  49844  line2ylem  50005