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  2998  necon4abid  3000  necon2abid  3002  necon2bbid  3003  necon1abii  3008  dfral2  3118  dfss6  3928  falseral0OLD  4478  difsnpss  4777  xpimasn  6185  2mpo0  7669  bropfvvvv  8093  zfregs2  9709  nqereu  10931  ssnn0fi  14041  swrdnnn0nd  14718  pfxnd0  14750  zeo4  16420  sumodd  16470  ncoprmlnprm  16811  numedglnl  29551  ballotlemfc0  34950  ballotlemfcc  34951  bnj1143  35245  bnj1304  35274  bnj1189  35464  bj-cbvaew  37325  wl-ifp-ncond2  38170  tsim1  38839  tsna1  38853  ecinn0  39062  aks4d1p7  42910  aks6d1c5  42966  onsupmaxb  44026  ifpxorcor  44262  ifpnot23b  44268  ifpnot23c  44270  ifpnot23d  44271  iunrelexp0  44488  expandrex  45062  con5VD  45668  sineq0ALT  45705  nepnfltpnf  46118  nemnftgtmnft  46120  sge0gtfsumgt  47217  atbiffatnnb  47709  ichnreuop  48281  islininds2  49323  nnolog2flm1  49429  line2ylem  49590