 Biconditional elimination rule

From $A\leftrightarrow B$, infer $A\to B$ or $B\to A$. Applying the resulting implication requires a further modus ponens rule.