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