# 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 $(P \leftrightarrow Q)$ is true, then one may infer that $(P \to Q)$ is true, and also that $(Q \to P)$ is true. 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: $\frac{(P \leftrightarrow Q)}{\therefore (P \to Q)}$

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

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

## Formal notation

The biconditional elimination rule may be written in sequent notation: $(P \leftrightarrow Q) \vdash (P \to Q)$

and $(P \leftrightarrow Q) \vdash (Q \to P)$

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

or as the statement of a truth-functional tautology or theorem of propositional logic: $(P \leftrightarrow Q) \to (P \to Q)$ $(P \leftrightarrow Q) \to (Q \to P)$

where $P$, and $Q$ are propositions expressed in some formal system.