Axiom ax-mp

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	$$⊢\phi$$
	maj	$$⊢\phi \to \psi$$
Assertion	ax-mp	$$⊢\psi$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wps	$$wff\psi$$