Biconditional elimination

Summary

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: