(A -> B) -> ~B -> ~A