dne

Theorem dne

Theorem. dne
¬¬A → A

Double negation elimination. It is not valid in intuitionistic logic, which is why it requires lem as a dependency.

Proof
01. 1 ⊢ ¬¬A, hypo.
02. ⊢ A ∨ ¬A, lem.
03. 3 ⊢ A, hypo.
04. 4 ⊢ ¬A, hypo.
05. 1, 4 ⊢ ⊥, neg_elim 1 4.
06. 1, 4 ⊢ A, efq 5.
07. 1 ⊢ A, disj_elim 2 3 6.
dne. ⊢ ¬¬A → A, subj_intro 7.

Dependencies
The given proof depends on two axioms:
efq, lem.