[A]1 [A → B]4 ---------------- [¬B]2 B ------------------- ⊥ --------- (1) [¬¬A]3 ¬A ---------------- ⊥ ------- (2) ¬¬B ----------- (3) ¬¬A → ¬¬B --------------------- (4) (A → B) → (¬¬A → ¬¬B)