If you have P and P → Q, conclude Q.
This is the oldest rule in logic — Aristotle knew it. Modus ponens ("the way of affirming") lets you apply an implication to its antecedent to obtain the consequent. It is the elimination rule for implication: you use an implication you already have.
P P → Q
——————————— →-Elim
Q
Two premises sit above the bar: the proposition P and the implication P → Q. Below the bar, the conclusion Q is obtained.
| Prover | Syntax |
|---|---|
| Lean 4 | exact h hp or apply h |
| Coq | apply H |
| Agda | h hp |
Given P → Q, Q → R, and P, construct the Gentzen tree for R.
Use →-Elim twice. First apply P → Q to P to get Q. Then apply Q → R to Q to get R.
P → Q Q → R
P P → Q |
——————————— →-Elim |
Q Q → R
——————————— →-Elim
R
The tree applies →-Elim twice: once to get Q from P and P → Q, and once to get R from Q and Q → R.
See also: Logic §02 — Implication | Strategies §01 — Direct proof