Theorem nnnotnotr 13872

Description: Double negation of double negation elimination. Suggested by an online post by Martin Escardo. Although this statement resembles nnexmid 840, 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 643	. 2 ⊢ (¬ (¬ ¬ 𝜑 → 𝜑) → ¬ 𝜑)
2		pm2.24 611	. . 3 ⊢ (¬ 𝜑 → (¬ ¬ 𝜑 → 𝜑))
3	2	con3i 622	. 2 ⊢ (¬ (¬ ¬ 𝜑 → 𝜑) → ¬ ¬ 𝜑)
4	1, 3	pm2.65i 629	1 ⊢ ¬ ¬ (¬ ¬ 𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 604  ax-in2 605

This theorem is referenced by: (None)