$(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)$.
Here is a proof using natural deduction in a Fitch-style proof checker. The proof is similar to what Joshua Taylor provided.



The inference rules used are disjunction introduction ($\lor$I), disjunction elimination ($\lor$E), implication introduction or conditional proof ($\to$I) and implication elimination or modus ponens ($\to$E).



Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/