Deduction of "Disjunction elimination" I have at my disposal Modus Ponens (MP) and the three axioms:


*

*A1: $(\alpha\to(\beta\to\alpha))$,

*A2: $((\alpha\to(\beta \to\gamma))\to ((\alpha\to\beta)\to(\alpha\to\gamma)))$,

*A3: $(((\lnot\beta)\to(\lnot\alpha))\to(((\lnot\beta)\to\alpha)\to\beta))$.


I'm trying to prove the Disjunction elimination:
$$
\{\alpha\lor\beta,\alpha\to \gamma,\beta\to \gamma\}\vdash \gamma.
$$
$\lor$ is not part of the alphabet I use, the deduction actually is:
$$
\{((\neg\alpha)\to\beta),\alpha\to \gamma,\beta\to \gamma\}\vdash \gamma.
$$
The deduction should be something like
\begin{array}{rl|l}
\hline
1:&((\neg\alpha)\to\beta)  & Premiss\\ 
2:&\beta\to \gamma&Premiss\\
3:&((\neg\alpha)\to\gamma)&1,2\ H.S.\\
4:&(\alpha \to \gamma)&Premiss\\
5:&\gamma& 3,4 [?]\\
\hline
\end{array}
Where H.S. is Hypothetical Syllogism, a deduction that I have already proven.

The rule $[?]$, that I have to prove, correspond to 
  $$
\{\alpha\to\beta,(\neg\alpha)\to\beta\}\vdash \beta.\tag{*}
$$

(*) looks quite simple, but after hours no way to get it.
For information I have, if needed, proven other results, that I could reuse:


*

*$\vdash\alpha\to\alpha$,

*Hypothetical Syllogism: $\{\alpha\to\beta,\beta\to\gamma\}\vdash\alpha\to\gamma$,

*$\vdash(\lnot\alpha\to\alpha)\to\alpha$,

*$\vdash\alpha\lor\lnot\alpha$,

*$\{\alpha\to(\beta\to\gamma),\beta\}\vdash\alpha\to\gamma$,

*$\vdash(\neg\neg\alpha)\to\alpha$.

*Negation introduction:
$\{(\alpha\to\beta),(\alpha\to \neg\beta)\}\vdash \neg \alpha$.

*Negation elimination:
$\{\neg \alpha\}\vdash (\alpha\to \beta)$.

*Double negative elimination:
$\neg \neg \alpha\vdash \alpha$.

*Conjunction introduction:
$\{\alpha,\beta\}\vdash (\alpha\land \beta)$.


EDIT Additional known results:


*

*$\neg\neg\alpha\vdash\alpha$

*$\{\alpha,\neg\alpha\}\vdash\neg\beta$

*$\{\alpha,\neg\alpha\}\vdash\beta$

*Conjunction elimination, only $\alpha\land\beta\vdash\beta$

*Disjunction introduction, only $\beta\vdash\alpha\lor\beta$

 A: Assuming you are allowed to use the Deduction Theorem:
Let's first prove Modus Tollens: $\varphi \rightarrow \psi, \neg \psi \vdash \neg \varphi$:


*

*$\varphi \rightarrow \psi$ Premise

*$\neg \psi$ Premise

*$\neg \psi \rightarrow (\neg \neg \varphi \rightarrow \neg \psi)$ A1

*$\neg \neg \varphi \rightarrow \neg \psi$ MP 2,3

*$\neg \neg \varphi \rightarrow \varphi$ Double Negation Elimination

*$\neg \neg \varphi \rightarrow \psi$ H.S. 1,5

*$(\neg \neg \varphi \rightarrow \neg \psi) \rightarrow ((\neg \neg \varphi \rightarrow \psi) \rightarrow \neg \varphi)$ A3

*$(\neg \neg \varphi \rightarrow \psi) \rightarrow \neg \varphi$ MP 4,7

*$\neg \varphi$ MP 6,8


With the Deduction Theorem, this gives us Contraposition: $\varphi \rightarrow \psi  \vdash \neg \psi \rightarrow \neg \varphi$
And now we can show $\varphi \rightarrow \psi, \neg \varphi \rightarrow \psi \vdash \psi$:


*

*$\varphi \rightarrow \psi$ Premise

*$\neg \varphi \rightarrow \psi$ Premise

*$\neg \psi \rightarrow \neg \varphi$ Contraposition 1

*$\neg \psi \rightarrow \neg \neg \varphi$ Contraposition 2

*$(\neg \psi \rightarrow \neg \neg \varphi) \rightarrow ((\neg \psi \rightarrow \neg \varphi) \rightarrow \psi)$ A3

*$(\neg \psi \rightarrow \neg \varphi) \rightarrow \psi$ MP 4,5

*$\psi$ MP 3,6

