Biconditional introduction rule
= Biconditional introduction rule
{title2=$\dfrac{\Gamma,A\vdash B\quad\Gamma,B\vdash A}{\Gamma\vdash A\leftrightarrow B}$}
Derive each side of a <logical biconditional> under a <temporary assumption> of the other, then discharge both assumptions. The surrounding assumptions $\Gamma$ remain. This is equivalent to deriving the two implications and combining them as the two directions of equivalence.