Le modus ponens, écrit

Posons $\Gamma =\{p,p\to q\}$.

$$\frac{\frac{}{\Gamma ⊢p\to q}\text{ax}\frac{}{\Gamma ⊢p}\text{ax}}{\Gamma ⊢q}{\to }_e$$

Trois nœuds, deux axiomes. La lecture se fait de bas en haut : le but $q$ est atomique, il n'y a donc pas de règle d'introduction à employer ; on cherche dans le contexte une hypothèse qui produise $q$, et c'est $p\to q$. La règle ${\to }_e$ demande alors deux prémisses, $\Gamma ⊢p\to q$ et $\Gamma ⊢p$, toutes deux dans le contexte : deux axiomes, et c'est fini.

Ce qu'il faut remarquer. Le contexte $\Gamma$ est le même sur les trois séquents. C'est la marque de ${\to }_e$ : elle ne décharge rien, elle consomme. La seule règle de ce chapitre qui modifie le contexte en montant est ${\to }_i$ — et ses cousines ${\neg }_i$ et ${\vee }_e$.

Et le lien avec le programme. Le B.O. cite le modus ponens comme premier exemple de règle dérivée. Il n'est pas une règle primitive de la déduction naturelle : c'est exactement l'élimination de l'implication, appliquée à deux axiomes.