क्या निम्नलिखित एक वैध inference नियम (tautology) है?

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

यह स्वचालित प्रमेय सिद्धि में उपयोग किया जाने वाला resolution नियम है।