Description: Rule of Modus Ponens. The postulated inference rule of propositional calculus. See, e.g., Rule 1 of Hamilton p. 73. The rule says, "if ph is true, and ph implies ps , then ps must also be true". This rule is sometimes called "detachment", since it detaches the minor premise from the major premise. "Modus ponens" is short for "modus ponendo ponens", a Latin phrase that means "the mode that by affirming affirms" - remark in Sanford p. 39. This rule is similar to the rule of modus tollens mto .
Note: In some web page displays such as the Statement List, the symbols " & " and " => " informally indicate the relationship between the hypotheses and the assertion (conclusion), abbreviating the English words "and" and "implies". They are not part of the formal language. (Contributed by NM, 30-Sep-1992)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | min | ⊢ 𝜑 | |
| maj | ⊢ ( 𝜑 → 𝜓 ) | ||
| Assertion | ax-mp | ⊢ 𝜓 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | wps | ⊢ 𝜓 |