# Modus Ponendo Ponens

## Proof Rule

The modus ponendo ponens is a valid deduction sequent in propositional logic:

If we can conclude $p \implies q$, and we can also conclude $p$, then we may infer $q$.

Thus it provides a means of eliminating a conditional from a sequent.

It can be written:

$\displaystyle {p \quad p \implies q \over q} \to_e$

### Sequent Form

The Modus Ponendo Ponens can be symbolised by the sequent:

$p \implies q, p \vdash q$

### Tableau Form

Let $\phi \implies \psi$ be a propositional formula in a tableau proof whose main connective is the implication operator.

The Modus Ponendo Ponens is invoked for $\phi \implies \psi$ and $\phi$ as follows:

 Pool: The pooled assumptions of $\phi \implies \psi$ The pooled assumptions of $\phi$ Formula: $\psi$ Description: Modus Ponendo Ponens Depends on: The line containing the instance of $\phi \implies \psi$ The line containing the instance of $\phi$ Abbreviation: $\text{MPP}$ or $\implies \mathcal E$

## Variants

The following forms can be used as variants of this theorem:

### Variant 1

$p \vdash \left({p \implies q}\right) \implies q$

### Variant 2

$\vdash p \implies \left({\left({p \implies q}\right) \implies q}\right)$

### Variant 3

$\vdash \left({\left({p \implies q}\right) \land p}\right) \implies q$

## Also known as

Modus ponendo ponens is also known as:

• Modus ponens
• The rule of implies-elimination
• The rule of material detachment.

## Linguistic Note

Modus ponendo ponens is Latin for mode that by affirming, affirms.

Modus ponens means mode that affirms.

## Also see

The following are related argument forms:

## Technical Note

When invoking Modus Ponendo Ponens in a tableau proof, use the ModusPonens template:

{{ModusPonens|line|pool|statement|first|second}}

or:

{{ModusPonens|line|pool|statement|first|second|comment}}

where:

line is the number of the line on the tableau proof where Modus Ponendo Ponens is to be invoked
pool is the pool of assumptions (comma-separated list)
statement is the statement of logic that is to be displayed in the Formula column, without the $...$ delimiters
first is the first of the two lines of the tableau proof upon which this line directly depends, the one in the form $p \implies q$
second is the second of the two lines of the tableau proof upon which this line directly depends, the one in the form $p$
comment is the (optional) comment that is to be displayed in the Notes column.