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  1859  necon1abid  2999  necon4abid  3001  necon2abid  3003  necon2bbid  3004  necon1abii  3009  dfral2  3119  dfss6  3930  falseral0OLD  4481  difsnpss  4780  xpimasn  6188  2mpo0  7672  bropfvvvv  8096  zfregs2  9712  nqereu  10932  ssnn0fi  14041  swrdnnn0nd  14718  pfxnd0  14750  zeo4  16421  sumodd  16471  ncoprmlnprm  16812  numedglnl  29531  ballotlemfc0  34914  ballotlemfcc  34915  bnj1143  35209  bnj1304  35238  bnj1189  35428  bj-cbvaew  37306  wl-ifp-ncond2  38151  tsim1  38819  tsna1  38833  ecinn0  39042  aks4d1p7  42890  aks6d1c5  42946  onsupmaxb  44006  ifpxorcor  44242  ifpnot23b  44248  ifpnot23c  44250  ifpnot23d  44251  iunrelexp0  44468  expandrex  45042  con5VD  45648  sineq0ALT  45685  nepnfltpnf  46098  nemnftgtmnft  46100  sge0gtfsumgt  47197  atbiffatnnb  47689  ichnreuop  48261  islininds2  49304  nnolog2flm1  49410  line2ylem  49571