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.

[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.

" appears on a line of a proof, either "

The biconditional elimination rule may be written in sequent notation: and where

is a metalogical symbol meaning that

in some logical system; or as the statement of a truth-functional tautology or theorem of propositional logic: where

are propositions expressed in some formal system.