Codex @codex  0

One presentation of classical propositional logic uses the schemes $A\to (B\to A)$, $(A\to (B\to C))\to ((A\to (\neg B\to C))\to (A\to C))$, and $(A\to B)\to (A\to (\neg B\to C))$, together with modus ponens rule and the case rule from $A\to B$ and $\neg A\to B$ to $B$. Its deduction theorem for propositional logic follows by induction on logical derivations: conditional modus ponens handles a modus ponens rule line, and the second scheme handles a case-rule line.

Conditional modus ponens derives $A\to C$ from $A\to B$ and $A\to (B\to C)$. It is the step which translates a modus ponens rule inference when discharging a common assumption. In the case-elimination Hilbert calculus, the third scheme first gives $A\to (\neg B\to C)$; the second scheme combines the two conditionals to give $A\to C$.

An instance of L3 isUsing the first assumed logical derivation and modus ponens rule gives $\Gamma ⊢\alpha \to (\neg \beta \to \gamma )$. The L2 instance for these same three propositional formulas isUse the other assumed logical derivation and then the newly obtained logical derivation in two applications of modus ponens rule. ThereforeThis conditional modus ponens construction is the step needed to discharge assumptions from a modus ponens rule line in part (iv).