Proof 01. 1 ⊢ ¬¬A → A, hypo. 02. 2 ⊢ ⊥, hypo. 03. 3 ⊢ ¬A, hypo. 04. 2, 3 ⊢ ⊥, wk 2. 05. 2 ⊢ ¬¬A, neg_intro 4. 06. 1, 2 ⊢ A, subj_elim 1 5. efq_from_dne. ⊢ (¬¬A → A) → (⊥ → A), subj_intro_ii 6.