Theorem contraposition_rev_ii

Proof
01. 1 ⊢ ¬A → ¬B → ¬C, hypo.
02. 2 ⊢ ¬A ∧ ¬B, hypo.
03. 2 ⊢ ¬A, conj_eliml 2.
04. 2 ⊢ ¬B, conj_elimr 2.
05. 1, 2 ⊢ ¬B → ¬C, subj_elim 1 3.
06. 1, 2 ⊢ ¬C, subj_elim 5 4.
07. 7 ⊢ C, hypo.
08. 1, 7, 2 ⊢ ⊥, neg_elim 6 7.
09. 1, 7 ⊢ ¬(¬A ∧ ¬B), neg_intro 8.
10. 1, 7 ⊢ ¬¬A ∨ ¬¬B, neg_conj 9.
11. 11 ⊢ ¬¬A, hypo.
12. 11 ⊢ A, dne 11.
13. 11 ⊢ A ∨ B, disj_introl 12.
14. 14 ⊢ ¬¬B, hypo.
15. 14 ⊢ B, dne 14.
16. 14 ⊢ A ∨ B, disj_intror 15.
17. 1, 7 ⊢ A ∨ B, disj_elim 10 13 16.
contraposition_rev_ii. ⊢ (¬A → ¬B → ¬C) → C → A ∨ B,
  subj_intro_ii 17.

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