ax-mp

Axiom. Rule of Modus Ponens.

Description:

The postulated inference rule of propositional calculus. See e.g. rule 1 of [Hamilton] p. 73. The rule says, "if phi is true, and phi implies psi, then psi must also be true." This rule is sometimes called "detachment", since it detaches the minor premise from the major premise.

Arguments:

phi (pr), psi (pr),

Hypotheses:

phi
(phitopsi)

Assertions:

psi