Tautology question

Question

I want to prove

(φ→ρ) → ((ψ→ρ) → ((φ∨ψ)→ρ))

I made a proof but don`t know doing right

may you check it whether doing right or wrong?

Answer 1

You should not be introducing a disjunction.   The elimination rule does not need to be belaboured.

• Assume $\varphi\to\rho$, $\psi\to \rho$, and $\varphi \vee\psi$.
• Eliminate the disjunction to deduce $\rho$.
• Discharge those three assumptions in turn to deduce $(\varphi\to\rho)\to((\psi\to \rho)\to((\varphi\vee\psi)\to\rho))$

That is all.

$$\dfrac{\dfrac{\dfrac{\dfrac{[\varphi\to \rho]^1\quad[\psi\to\rho]^2\quad [\varphi\vee\psi]^3}{\rho}{\small\vee\mathsf E}}{(\varphi\vee\psi)\to\rho}{\small\to\mathsf I^3}}{(\psi\to \rho)\to((\varphi\vee\psi)\to\rho)}{\small\to\mathsf I^2}}{(\varphi\to\rho)\to((\psi\to \rho)\to((\varphi\vee\psi)\to\rho))}{\small\to\mathsf I^1}$$

Really, all this proof is doing is saying "This can be justified as a tautology by accepting the disjunctive elimination and conditional introduction rules."

$$\begin{split}\varphi\to\rho, \psi\to \rho, \varphi \vee\psi & \vdash \rho\\\hline &\vdash (\varphi\to\rho)\to((\psi\to \rho)\to((\varphi \vee\psi) \to\rho))\end{split}$$