Theorem notnot 135

Description: Double negation introduction. Converse of notnotr 124 and one implication of notnotb 303. Theorem *2.12 of [WhiteheadRussell] p. 101. This was the sixth axiom of Frege, specifically Proposition 41 of [Frege1879] p. 47. (Contributed by NM, 28-Dec-1992.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)

Assertion

Ref	Expression
notnot	⊢ (𝜑 → ¬ ¬ 𝜑)

Proof of Theorem notnot

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (¬ 𝜑 → ¬ 𝜑)
2	1	con2i 133	1 ⊢ (𝜑 → ¬ ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  notnoti  136  notnotd  137  con1d  138  con4iOLD  144  notnotb  303  biortn  420  pm2.13  433  nfnt  1767  necon2ad  2797  necon4ad  2801  necon4ai  2813  eueq2  3347  ifnot  4083  nbusgra  25957  wlkntrl  26092  eupath2  26507  knoppndvlem10  31682  wl-orel12  32473  cnfn1dd  33064  cnfn2dd  33065  axfrege41  37158  vk15.4j  37755  zfregs2VD  38098  vk15.4jVD  38172  con3ALTVD  38174  stoweidlem39  38932