¿Es la siguiente una regla de inferencia válida (tautología)?

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

Esta es la regla de resolución utilizada en la demostración automática de teoremas.