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  is true, then one may infer that  is true, and also that  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:

and

where the rule is that wherever an instance of "" appears on a line of a proof, either "" or "" can be placed on a subsequent line;

Formal notation 
The biconditional elimination rule may be written in sequent notation:

and

where  is a metalogical symbol meaning that , in the first case, and  in the other are syntactic consequences of  in some logical system;

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

where , and  are propositions expressed in some formal system.

See also
 Logical biconditional

References

Rules of inference
Theorems in propositional logic