# Modus Ponendo Ponens/Proof Rule

## Proof Rule

Modus ponendo ponens is a valid argument in types of logic dealing with conditionals $\implies$.

This includes propositional logic and predicate logic, and in particular natural deduction.

As a proof rule it is expressed in the form:

If we can conclude $\phi \implies \psi$, and we can also conclude $\phi$, then we may infer $\psi$.

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

It can be written:

$\ds {\phi \qquad \phi \implies \psi \over \psi} \to_e$

### Tableau Form

Let $\phi \implies \psi$ be a well-formed 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 \EE$

## Also known as

Modus Ponendo Ponens is also known as:

• Modus ponens, abbreviated M.P.
• The rule of implies-elimination
• The rule of arrow-elimination
• The rule of (material) detachment
• The process of inference

## Linguistic Note

Modus Ponendo Ponens is Latin for mode that by affirming, affirms.

The shorter form Modus Ponens means mode that affirms.

## 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.