# Biconditional Elimination/Proof Rule/Tableau Form

## Proof Rule

Let $\phi \iff \psi$ be a propositional formula] in a tableau proof whose main connective is the biconditional operator.

Biconditional Elimination is invoked for $\phi \iff \psi$ in either of the two forms:

Form 1
 Pool: The pooled assumptions of $\phi \iff \psi$ Formula: $\phi \implies \psi$ Description: Biconditional Elimination Depends on: The line containing $\phi \iff \psi$ Abbreviation: $\mathrm {BE}_1$ or $\iff \EE_1$

Form 2
 Pool: The pooled assumptions of $\phi \iff \psi$ Formula: $\psi \implies \phi$ Description: Biconditional Elimination Depends on: The line containing $\phi \iff \psi$ Abbreviation: $\mathrm {BE}_2$ or $\iff \EE_2$

## Also denoted as

Sources which refer to this rule as the biconditional-conditional rule may as a consequence give the abbreviation $\mathrm {BC}$.