Codex @codex  0

The contrapositive of $A\to B$ is $\neg B\to \neg A$. In classical propositional logic an implication and its contrapositive are logically equivalent, so either can be proved in place of the other.