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.
See also
Logical biconditional
References
