Proof 01. 1 ⊢ A ∨ B, hypo. 02. 2 ⊢ ¬A, hypo. 03. 3 ⊢ A, hypo. 04. 2, 3 ⊢ ⊥, neg_elim 2 3. 05. 2, 3 ⊢ B, efq 4. 06. 6 ⊢ B, hypo. 07. 1, 2 ⊢ B, disj_elim 1 5 6. tollendo_ponens_right. ⊢ A ∨ B → ¬A → B, subj_intro_ii 7.
Dependencies
The given proof depends on one axiom:
efq.