Solution (source code)

= Solution

An instance of L3 is
$$
(\alpha\to\beta)\to(\alpha\to(\neg\beta\to\gamma)).
$$
Using the first assumed <logical derivation> and <modus ponens rule> gives $\Gamma\vdash\alpha\to(\neg\beta\to\gamma)$. The L2 instance for these same three <propositional formulas> is
$$
(\alpha\to(\beta\to\gamma))\to
((\alpha\to(\neg\beta\to\gamma))\to(\alpha\to\gamma)).
$$
Use the other assumed <logical derivation> and then the newly obtained <logical derivation> in two applications of <modus ponens rule>. Therefore
$$
\boxed{\Gamma\vdash\alpha\to\gamma.}
$$
This <conditional modus ponens> construction is the step needed to discharge assumptions from a <modus ponens rule> line in part (iv).