$(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$?
 A: HINT: $(P\to Q)\to\lnot P\lor Q\lor R\equiv(P\to Q)\to((P\to Q)\lor R)$.
A: You can take benefit of the fact that :

$(A \implies B)$ is equivalent to $(\lnot A \lor B)$

so that, e.g

$(R \lor P)$ will be $(\lnot R \implies P)$.

Now, if you rewrite your formula in this way, you will get :

$$(P \implies Q) \implies [ (\lnot R \implies P) \implies (\lnot R \implies Q)]$$

and this is a version of Hypothetical Syllogism.
A: P   Q   R   (P-->Q)   (R V P)  (R V Q)  [(R V P) --> (R V Q)] {(P-->Q) ->[(R V P)-->(R V Q)]}

T   T   T     T          T        T               T                     T

T   T   F     T          T        T               T                     T

T   F   T     F          T        T               T                     T

T   F   F     F          T        F               F                     T

F   T   T     T          T        T               T                     T

F   T   F     T          F        T               T                     T

F   F   T     T          T        T               T                     T

F   F   F     T          F        F               T                     T

The last column as all the T's which means your statement is a tautology. This is probably easier to do than use equivalent statements.
A: This is relatively straightforward with natural deduction:


*

*1.  Suppose $P \to Q$.

*

*2. Suppose $R \lor P$.

*

*3. Suppose $R$.

*

*4. $R \lor Q$ by $\lor$-introduction with 3.


*5. Suppose $P$.

*

*6. $Q$ by $\to$-elimination with 1 and 5.

*7. $R \lor Q$ by $\lor$-introduction with 6.


*8. $R \lor Q$ by $\lor$-elimination with 2, 3–4, and 5–7.


*9. $(R \lor P) \to (R \lor Q)$ by $\to$-introduction with 2–8.


*10. $(P \to Q) \to ((R\lor P) \to (R \lor Q))$ by $\to$-introduction with 1–9.

A: Suppose that $P$ implies $Q$. This means that either (i) $P$ is false (and we don't care about $Q$) or (ii) $P$ is true and $Q$ true. In either case, we don't care about $R$; it's a red herring. So in case (i), $P$ is false, so that $\neg P\lor Q\lor R$  is true. In case (ii), $Q$ is true (and so is $P$, but we don't really care in this case), so that $\neg P\lor Q\lor R$ is true, again.
To sum up, ($P\Longrightarrow Q$) logically implies $\neg P\lor Q\lor R$.
A: One way to do this is with the method of analytic tableaux, described in detail in M D’Agostino's Handbook of Tableaux Methods. This approach is somewhat informal but what it produces is often very suggestive of a proof (and is even equivalent to one in many semantics).
We start with the negation of $$(P\to Q)\to ((R\vee P)\to (R\vee Q))\tag{1}$$ then apply a series of contradiction-hunting rules to show that the negation is always false. Look:
.
This ends in contradictions. Thus $(1)$ is indeed a tautology.
I hope that helps $\ddot\smile$
A: 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/
