The contrapositive of an implication $$P\Rightarrow Q$$ is the implication $${\rm not}(Q)\Rightarrow{\rm not}(P)\text{,}$$ where “not” means the logical negation, or opposite. An implication is true if and only if its contrapositive is true. In symbols, $$(P\Rightarrow Q)\iff({\rm not}(Q)\Rightarrow{\rm not}(P))$$ is a theorem. Such statements about logic, that are always true, are known as tautologies.