modus ponens
Modus ponens^{} is a rule of inference^{} that is commonly found in many logics where the binary logical connective $\to $ (sometimes written $\Rightarrow $ or $\supset $) called logical implication are defined. Informally, it states that
from $A$ and $A\to B$, we may infer $B$.
Modus ponens is also called the rule of detachment: the theorem^{} $b$ can be “detached” from the theorem $A\to B$ provided that $A$ is also a theorem.
An example of this rule is the following: From the premisses “It is raining”, and “If it rains, then my laundry will be soaked”, we may draw the conclusion^{} “My laundry will be soaked”.
Two common ways of mathematically denoting modus ponens are the following:
$$\frac{A\mathit{\hspace{1em}}A\to B}{B}\mathit{\hspace{1em}\hspace{1em}}\text{or}\mathit{\hspace{1em}}\{A,A\to B\}\u22a2B.$$ 
One formal way of looking at modus ponens is to define it as a partial function^{} $\u22a2:F\times F\to F,$ where $F$ is a set of formulas^{} in a language^{} $L$ where a binary operation^{} $\to $ is defined, such that

1.
$\u22a2(A,B)$ is defined whenever $A,B\in F$ and $B\equiv (A\to C)$ for some $C\in L$, and

2.
when this is the case, $C\in F$ and $\u22a2(A,B):=C$;

3.
$\u22a2$ is not defined otherwise.
Remark. With modus ponens, one can easily prove the converse^{} of the deduction theorem^{} (see this link (http://planetmath.org/DeductionTheorem)). Another easily proven fact is the following:
If $\mathrm{\Delta}\u22a2A$ and $\mathrm{\Delta}\u22a2A\to B$, then $\mathrm{\Delta}\u22a2B$, where $\mathrm{\Delta}$ is a set of formulas.
To see this, let ${A}_{1},\mathrm{\dots},{A}_{n}$ be a deduction^{} of $A$ from $\mathrm{\Delta}$, and ${B}_{1},\mathrm{\dots},{B}_{m}$ be a deduction of $A\to B$ from $\mathrm{\Delta}$. Then ${A}_{1},\mathrm{\dots},{A}_{n},{B}_{1},\mathrm{\dots},{B}_{m},B$ is a deduction of $B$ from $\mathrm{\Delta}$, where $B$ is inferred from ${A}_{n}$ (which is $A$) and ${B}_{m}$ (which is $A\to B$) by modus ponens.
Title  modus ponens 

Canonical name  ModusPonens 
Date of creation  20130322 16:50:48 
Last modified on  20130322 16:50:48 
Owner  CWoo (3771) 
Last modified by  CWoo (3771) 
Numerical id  19 
Author  CWoo (3771) 
Entry type  Definition 
Classification  msc 03B22 
Classification  msc 03B05 
Classification  msc 03B35 
Synonym  rule of detachment 
Synonym  detachment 
Synonym  modus ponendo ponens 