Two rules are automatically derived from this
theorem. When applied to one argument, the contraposition rule
(H ⊢ A → B) → (H ⊢ ¬B → ¬A),
and when applied to two arguments, the modus tollens
(H1 ⊢ A → B) → (H2 ⊢ ¬B) → (H1 ∧ H2 ⊢ ¬A).
Proof sketch
From the premises A → B and ¬B we need to derive the conclusion ¬A.
This means, from the additional premise A we need to derive a
contradiction. First, B follows from A → B and A. But then we have
both ¬B and B, which is already a contradiction. q.e.d.
Proof 01. 1 ⊢ ¬B, hypo. 02. 2 ⊢ A → B, hypo. 03. 3 ⊢ A, hypo. 04. 2, 3 ⊢ B, subj_elim 2 3. 05. 1, 2, 3 ⊢ ⊥, neg_elim 1 4. 06. 2, 1 ⊢ ¬A, neg_intro 5. 07. 2 ⊢ ¬B → ¬A, subj_intro 6. contraposition. ⊢ (A → B) → ¬B → ¬A, subj_intro 7.