 Case-elimination Hilbert calculus

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.