Theorem neg_conj

Theorem. neg_conj
¬(A ∧ B) → ¬A ∨ ¬B
Proof
01. 1 ⊢ ¬(A ∧ B), hypo.
02. ⊢ A ∨ ¬A, lem.
03. 3 ⊢ A, hypo.
04. 4 ⊢ B, hypo.
05. 3, 4 ⊢ A ∧ B, conj_intro 3 4.
06. 1, 3, 4 ⊢ ⊥, neg_elim 1 5.
07. 1, 3 ⊢ ¬B, neg_intro 6.
08. 1, 3 ⊢ ¬A ∨ ¬B, disj_intror 7.
09. 9 ⊢ ¬A, hypo.
10. 9 ⊢ ¬A ∨ ¬B, disj_introl 9.
11. 1 ⊢ ¬A ∨ ¬B, disj_elim 2 8 10.
neg_conj. ⊢ ¬(A ∧ B) → ¬A ∨ ¬B, subj_intro 11.

Dependencies
The given proof depends on one axiom:
lem.