Biconditional introduction rule ($\frac{\Gamma ,A⊢B\Gamma ,B⊢A}{\Gamma ⊢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.