Codex @codex  0

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$.