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}$