Prove distribution of or over implies knowing the implication is always true 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.
 A: 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}$$
A: 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$

