Prove distribution of or over implies knowing the implication is always true

Question

I was given a task to construct a Hilbert-style proof for the following:

$A → B ⊢ C ∨ A → C ∨ B$

I figured I could use the axiom $A→B≡A∨B≡B$, but this leads me nowhere since I don't think I can use the consequent anywhere.

The theorem is intuitively true to me (since we know $A→B$, adding a true $C$ in there will give $⊤→⊤$, obviously true, and a false $C$ gives the original $A→B$), but I do not know how to prove this.

I'm using Tourlakis' Mathematical Logic and all axioms contained within it.

Answer 1

Here are the relevant Hilbert Axiom Schemas...(your book may label them differently, or treat disjunction as a substitution.)

$$\begin{array}{rl}\mathrm A2.&\phi\to(\psi\to\phi) \\ \mathrm A3.&(\phi\to(\psi\to\xi))\to((\phi\to\psi)\to(\phi\to\xi)) \\ \lor\mathrm {IL}.&\phi\to(\phi\lor\psi) \\ \lor\mathrm {IR}.&\phi\to(\psi\lor\phi) \\ \lor\mathrm E.&(\phi\to\xi)\to((\phi\to\xi)\to((\phi\lor\psi)\to\xi)) \\\hdashline \mathrm P1.&A\to B \\\hline 2.&\lower{2ex}\ddots\end{array}$$

Answer 2

1) $A \to B \ \ \ \ \ \langle \text { assumption } \rangle$

2) $ C \lor A \ \ \ \ \ \ \langle \text { assumption } \rangle$

3) $C \lor A \equiv \lnot C \to A \ \ \ \ \langle 2.4.11 \rangle$

4) $\lnot C \to A \ \ \ \ \langle (2,3) + \text {Eqn} \rangle$

5) $\lnot C \to B \ \ \ \ \langle (2.5.9 \text { Coroll. - Transitivity of} \to) \rangle$

6) $C \lor B \equiv \lnot C \to B \ \ \ \ \langle 2.4.11 \rangle$

7) $C \lor B \ \ \ \ \langle (5,6) + \text {Eqn} \rangle$

8) $C \lor A \to C \lor B \ \ \ \langle (2.6.1 \text { Deduction Theorem}) \rangle$