 Biconditional introduction rule

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.