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 ↔ Q ) is true, then one may infer that ( P → Q ) is true, and also that ( Q → 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:
( P ↔ Q ) ∴ ( P → Q ) and
( P ↔ Q ) ∴ ( Q → P ) where the rule is that wherever an instance of " ( P ↔ Q ) " appears on a line of a proof, either " ( P → Q ) " or " ( Q → P ) " can be placed on a subsequent line;
The biconditional elimination rule may be written in sequent notation:
( P ↔ Q ) ⊢ ( P → Q ) and
( P ↔ Q ) ⊢ ( Q → P ) where ⊢ is a metalogical symbol meaning that ( P → Q ) , in the first case, and ( Q → P ) in the other are syntactic consequences of ( P ↔ Q ) in some logical system;
or as the statement of a truth-functional tautology or theorem of propositional logic:
( P ↔ Q ) → ( P → Q ) ( P ↔ Q ) → ( Q → P ) where P , and Q are propositions expressed in some formal system.
