The contrapositive of an implication (A -> B) is (NOT B -> NOT A). These two statements are equivalent by the following proof:

Statement            Reason
A -> B               Premise
NOT A OR B           A definition of implication
B OR NOT A           Commutative Law of logical OR
NOT NOT B OR NOT A   Law of Double Negation
NOT B -> NOT A       A definition of implication

Here is a truth table of an implication a implies b and its contrapositive not b implies not a. Also shown are the statements not a or b and not a or not not b:

 a | b | not a | not b | a --> b | not b --> not a | not a or b | not a or not not b
-------------------------------------------------------------------------------------
 T | T |   F   |   F   |    T    |        T        |     T      |          T
 T | F |   F   |   T   |    F    |        F        |     F      |          F
 F | T |   T   |   F   |    T    |        T        |     T      |          T
 F | F |   T   |   T   |    T    |        T        |     T      |          T

Note also converse and inverse. Just as an implication is logically equivalent to its contrapositive, the converse of the implication is logically equivalent to its inverse. When considering a proof, the contrapositive may be an easier thing to prove than the original implication, for whatever reason.