Users' Mathboxes Mathbox for Jim Kingdon < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  nnnotnotr GIF version

Theorem nnnotnotr 13990
Description: Double negation of double negation elimination. Suggested by an online post by Martin Escardo. Although this statement resembles nnexmid 845, 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
StepHypRef Expression
1 conax1 648 . 2 (¬ (¬ ¬ 𝜑𝜑) → ¬ 𝜑)
2 pm2.24 616 . . 3 𝜑 → (¬ ¬ 𝜑𝜑))
32con3i 627 . 2 (¬ (¬ ¬ 𝜑𝜑) → ¬ ¬ 𝜑)
41, 3pm2.65i 634 1 ¬ ¬ (¬ ¬ 𝜑𝜑)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 609  ax-in2 610
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator