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