The contrapositive of an implication p ⇒ q is the implication ¬q ⇒ ¬p. An implication and its contrapositive are logically equivalent, so that one is true if and only if the other is. For example, the theorem that if n² is odd then n is odd could be proved by showing instead that if n is even then n² is even.