contraposition

Theorem contraposition

Theorem. contraposition
(A → B) → ¬B → ¬A

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.