Biconditional elimination

${\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)⊢(P\to Q)}$

and

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

where ${\displaystyle ⊢}$ 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.