Contrapositive ($\neg B\to \neg A$)

The contrapositive of a logical implication $A\to B$ reverses the direction and applies logical negation to both sides: $\neg B\to \neg A$. In classical propositional logic they are equivalent, so either can be proved in place of the other. The contrapositive of “divisibility by four implies being an even number” says that a number that is not an even number cannot be divisible by four.

In Intuitionistic propositional logic, $A\to B$ still implies its contrapositive: assumptions $A$ and $\neg B$ would yield $B$ and hence a contradiction. The reverse direction is not generally valid. From $\neg B\to \neg A$ and $A$, one obtains only $\neg \neg B$; obtaining $B$ additionally requires double-negation elimination.