Conditional modus ponens ($\Gamma ⊢A\to B,A\to (B\to C)⟹\Gamma ⊢A\to C$)

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