# Biconditional elimination

Biconditional elimination is the name of two valid rules of inference of propositional logic. It allows for one to infer a conditional from a biconditional. If ${\displaystyle (P\leftrightarrow Q)}$ is true, then one may infer that ${\displaystyle (P\to Q)}$ is true, and also that ${\displaystyle (Q\to P)}$ is true.[1] For example, if it's true that I'm breathing if and only if I'm alive, then it's true that if I'm breathing, I'm alive; likewise, it's true that if I'm alive, I'm breathing. The rules can be stated formally as:

${\displaystyle {\frac {(P\leftrightarrow Q)}{\therefore (P\to Q)}}}$

and

${\displaystyle {\frac {(P\leftrightarrow Q)}{\therefore (Q\to P)}}}$

where the rule is that wherever an instance of "${\displaystyle (P\leftrightarrow Q)}$" appears on a line of a proof, either "${\displaystyle (P\to Q)}$" or "${\displaystyle (Q\to P)}$" can be placed on a subsequent line;

## Formal notation

The biconditional elimination rule may be written in sequent notation:

${\displaystyle (P\leftrightarrow Q)\vdash (P\to Q)}$

and

${\displaystyle (P\leftrightarrow Q)\vdash (Q\to P)}$

where ${\displaystyle \vdash }$ is a metalogical symbol meaning that ${\displaystyle (P\to Q)}$, in the first case, and ${\displaystyle (Q\to P)}$ in the other are syntactic consequences of ${\displaystyle (P\leftrightarrow Q)}$ in some logical system;

or as the statement of a truth-functional tautology or theorem of propositional logic:

${\displaystyle (P\leftrightarrow Q)\to (P\to Q)}$
${\displaystyle (P\leftrightarrow Q)\to (Q\to P)}$

where ${\displaystyle P}$, and ${\displaystyle Q}$ are propositions expressed in some formal system.