Given an implication of the form $$p \implies q$$ (``p implies q'') the contrapositive of this implication is $$\neg q \implies \neg p$$ (``not q implies not p'').

An implication and its contrapositive are equivalent statements. When proving a theorem, it is often more convenient or more intuitive to prove the contrapositive instead.