Modus ponens

In propositional logic, modus ponendo ponens (Latin for "the way that affirms by affirming"; generally abbreviated to MP or modus ponens) or implication elimination is a rule of inference. It can be summarized as "P implies Q and P is asserted to be true, so therefore Q must be true." The history of modus ponens goes back to antiquity.

Modus ponens is closely related to another valid form of argument, modus tollens. Both have apparently similar but invalid forms such as affirming the consequent, denying the antecedent, and evidence of absence. Constructive dilemma is the disjunctive version of modus ponens. Hypothetical syllogism is closely related to modus ponens and sometimes thought of as "double modus ponens."

The modus ponens rule may be written in sequent notation:

where ⊢ is a metalogical symbol meaning that Q is a syntactic consequence of P → Q and P in some logical system;

or as the statement of a truth-functional tautology or theorem of propositional logic:

where P, and Q are propositions expressed in some formal system.

The argument form has two premises (hypothesis). The first premise is the "if–then" or conditional claim, namely that P implies Q. The second premise is that P, the antecedent of the conditional claim, is true. From these two premises it can be logically concluded that Q, the consequent of the conditional claim, must be true as well. In artificial intelligence, modus ponens is often called forward chaining.

...
Wikipedia