Är följande en giltig slutledningsregel (tautologi)?

((A ∨ B) ∧ (¬B ∨ C)) → (A ∨ C)

Detta är resolutionsregeln som används inom automatiserad teorembevisning.