Conditional modus ponens
= Conditional modus ponens
{title2=$\Gamma\vdash A\to B,\ A\to(B\to C)\Longrightarrow\Gamma\vdash 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$.