# Modus Tollendo Tollens/Proof Rule/Tableau Form

Let $\phi \implies \psi$ be a propositional formula in a tableau proof whose main connective is the implication operator.
The Modus Tollendo Tollens is invoked for $\phi \implies \psi$ and $\neg \psi$ as follows:
 Pool: The pooled assumptions of $\phi \implies \psi$ The pooled assumptions of $\neg \psi$ Formula: $\neg \phi$ Description: Modus Tollendo Tollens Depends on: The line containing the instance of $\phi \implies \psi$ The line containing the instance of $\neg \psi$ Abbreviation: $\text{MTT}$