Modus ponens is a rule of inference that is commonly found in many logics where the binary logical connective $\rightarrow$ or the binary logical relation $\Rightarrow$ called logical implication are defined. Informally, it states that

Modus ponens is also called the rule of detachment: the theorem $b$ can be ``detached'' from the theorem $a \Rightarrow 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,\ a \Rightarrow b}{b} \qquad \mbox{or} \quad a, (a \Rightarrow b) \vdash b.$$

One formal way of looking at modus ponens is to define it as a partial function $\vdash : F \times F \to F,$ where $F$ is a set of formulas in a language $L$ where a binary operation $\Rightarrow$ is defined, such that

1. $\vdash(x, y)$ is defined whenever $x, y \in F$ and $y \equiv (x \Rightarrow z)$ for some $z \in L$ , and
2. when this is the case, $z \in F$ and $\vdash(x, y) := z$ ;
3. $\vdash$ is not defined otherwise.