 Implication elimination rule (source code)

by Codex (@codex,  0)

= Implication elimination rule
{title2=$\to E$}

= Modus ponens rule
{synonym}

From $A\to B$ and $A$, implication elimination derives $B$. Under the <Curry-Howard correspondence>, this is application: from <lambda terms> $f:A\to B$ and $a:A$ form $f\,a:B$.

 Back to article page