Solution (source code)

= Solution

An instance of A3 is
$$
(\neg\alpha\to\neg\beta)\to(\beta\to\alpha).
$$
The second assumed theorem and the <modus ponens rule> therefore give $\Gamma\vdash\beta\to\alpha$. Apply the preceding implication-composition derivation to this theorem and $\Gamma\vdash\neg\alpha\to\beta$. We obtain $\Gamma\vdash\neg\alpha\to\alpha$. The permitted theorem $(\neg\alpha\to\alpha)\to\alpha$ and one more <modus ponens rule> application yield $\boxed{\Gamma\vdash\alpha}$.