Do we know something about this refutation method for SAT?
As far as I can tell the earliest mention of the procedure you outline, later described in the literature as variable elimination by clause distribution, was in the paper "ZRes: The old Davis-Putnam procedure meets ZBDD" by Philippe Chatalic and Laurent Simon.  The procedure was described again, along with other formula simplification techniques, in "Effective Preprocessing in SAT through Variable and Clause Elimination" by Niklas Eén and Armin Biere.

The procedure was shown to be a workable way to improve SAT solver performance if care is taken to minimize clause growth as the implicants of removed terms are distributed, or to use data structures that efficiently manage large clause sets.