$(P\implies Q) \implies [(R ∨ P)\implies (R ∨ Q)]$ is a tautology I'm currently trying to work on the proof for this tautology.
But every time I derive the right side, I end up with a lone $R$ that will never cancel out.
Like I always end up with
$$(P\implies Q) \implies  ¬P∨Q∨R$$
And the $R$ never goes away at this point.
What can I do to cancel out the $R$?

HINT: $(P\to Q)\to\lnot P\lor Q\lor R\equiv(P\to Q)\to((P\to Q)\lor R)$.
