Biconditional introduction (↔I) is a basic rule of inference in logic by which a biconditional, or iff (if and only if), statement is formed out of two certain conditionals. The biconditional introduction rule holds that when both "if P then Q" and "if Q then P" are true, then "if and only if P, then Q" is also true.
The biconditional introduction rule may be formally presented as follows:
α → β, β → α 
α ↔ β