Theorem contraposition_rev

Proof
01. 1 ⊢ ¬A → ¬B, hypo.
02. 1 ⊢ ¬¬B → ¬¬A, contraposition 1.
03. 3 ⊢ B, hypo.
04. 3 ⊢ ¬¬B, dn_intro 3.
05. 1, 3 ⊢ ¬¬A, subj_elim 2 4.
06. 1, 3 ⊢ A, dne 5.
07. 1 ⊢ B → A, subj_intro 6.
contraposition_rev. ⊢ (¬A → ¬B) → (B → A), subj_intro 7.

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