Biconditional (minmal logic)

Introduction Rule

$\frac{\begin{array}{cc}[A{]}_i& [B{]}_i\\ ⋮& ⋮\\ A& B\end{array}}{A⟺B}i$

Elimination Rule

$\frac{AA⟺B}{B}$ $\frac{BA⟺B}{A}$