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.