# Modus Tollendo Ponens/Proof Rule/Tableau Form

## Proof Rule

Let $\phi \lor \psi$ be a well-formed formula in a tableau proof whose main connective is the disjunction operator.

The Modus Tollendo Ponens is invoked for $\phi \lor \psi$ in either of the two forms:

Form 1
 Pool: The pooled assumptions of $\phi \lor \psi$ The pooled assumptions of $\neg \phi$ Formula: $\psi$ Description: Modus Tollendo Ponens Depends on: The line containing the instance of $\phi \lor \psi$ The line containing the instance of $\neg \phi$ Abbreviation: $\text{MTP}_1$

Form 2
 Pool: The pooled assumptions of $\phi \lor \psi$ The pooled assumptions of $\neg \psi$ Formula: $\phi$ Description: Modus Tollendo Ponens Depends on: The line containing the instance of $\phi \lor \psi$ The line containing the instance of $\neg \psi$ Abbreviation: $\text{MTP}_2$