[p → (q ∨ r)] ∧ (~q)} → (p → r) = ((p' + q + r)q')' + p' + r = (p'q' + rq')' + p' + r = (p + q)(r' + q) + p' + r = pr' + pq + qr' + q + p' + r =pr' + (pq + qr' +q) + p' + r = (pr' + p') + q(p + r' +1) + r = p' +r' + q + r =p' + q + (r + r') = p' + q + T = TAUTOLOGY