Theorem neg_subj

Proof
01. 1 ⊢ B, hypo.
02. 2 ⊢ A, hypo.
03. 1, 2 ⊢ B, wk 1.
04. 1 ⊢ A → B, subj_intro 3.
05. 5 ⊢ ¬(A → B), hypo.
06. 5, 1 ⊢ ⊥, neg_elim 5 4.
07. 5 ⊢ ¬B, neg_intro 6.
08. 8 ⊢ ¬A, hypo.
09. 9 ⊢ A, hypo.
10. 8, 9 ⊢ ⊥, neg_elim 8 9.
11. 8, 9 ⊢ B, efq 10.
12. 8 ⊢ A → B, subj_intro 11.
13. 5, 8 ⊢ ⊥, neg_elim 5 12.
14. 5 ⊢ ¬¬A, neg_intro 13.
15. 5 ⊢ A, dne 14.
16. 5 ⊢ A ∧ ¬B, conj_intro 15 7.
neg_subj. ⊢ ¬(A → B) → A ∧ ¬B, subj_intro 16.

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