Fairness abstractions are useful for reasoning about computations of nondeterministic programs. This paper presents proof rules for reasoning about three fairness notions and one safety assumption with an automated theorem prover. These proof rules have been integrated into a mechanization of the Unity logic [8,9] and are suitable for the mechanical verification of concurrent programs. Mechanical verification provides greater trust in the correctness of a proof.