Theorem nnnotnotr 17016

Description: Double negation of double negation elimination. Suggested by an online post by Martin Escardo. Although this statement resembles nnexmid 862, it can be proved with reference only to implication and negation (that is, without use of disjunction). (Contributed by Jim Kingdon, 21-Oct-2024.)

Assertion

Ref	Expression
nnnotnotr	⊢ ¬ ¬ (¬ ¬ 𝜑 → 𝜑)

Proof of Theorem nnnotnotr

Step	Hyp	Ref	Expression
1		conax1 663	. 2 ⊢ (¬ (¬ ¬ 𝜑 → 𝜑) → ¬ 𝜑)
2		pm2.24 630	. . 3 ⊢ (¬ 𝜑 → (¬ ¬ 𝜑 → 𝜑))
3	2	con3i 641	. 2 ⊢ (¬ (¬ ¬ 𝜑 → 𝜑) → ¬ ¬ 𝜑)
4	1, 3	pm2.65i 648	1 ⊢ ¬ ¬ (¬ ¬ 𝜑 → 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 623  ax-in2 624

This theorem is used by: (None)