Biconditional elimination (↔E) is a basic rule of inference in logic by which a proposition or formula is derived from a biconditional, or iff (if and only if), statement when one formula or proposition in the biconditional is known. The biconditional elimination rule states that when "if and only if P then Q", if "P" (or "Q") is true, then "Q" (or "P") must be true.
The biconditional elimination rule may be formally presented as follows:
α ↔ β, α 
β
…and:
α ↔ β, β α