Remove unneeded atoms in CNF minimalization (SAT preprocessing)
As Kyle Jones has mentioned, the example you provided is called (restricted) resolution. 

Beside that, pure literals can also be safely removed from a SAT problem. Unit clauses can be assigned a truth value. Check this paper:

The Puzzling Role of Simplification in Propositional Satisfiability.  Inês Lynce and João Marques-Silva.

It discusses several preprocessing techniques for SAT, and its experiments showed that applying preprocessing for SAT leads to mix results. However, this paper might not be state-of-the-art.