= Solution
Use a <biconditional introduction rule> that discharges the two displayed temporary assumptions:
$$
\boxed{\frac{\Gamma,A\vdash B\qquad\Gamma,B\vdash A}{\Gamma\vdash A\leftrightarrow B}.}
$$
Suitable elimination rules are
$$
\boxed{\frac{\Gamma\vdash A\leftrightarrow B\qquad\Gamma\vdash A}{\Gamma\vdash B},\qquad
\frac{\Gamma\vdash A\leftrightarrow B\qquad\Gamma\vdash B}{\Gamma\vdash A}.}
$$
These are equivalent to using the <biconditional elimination rule> to extract the two implications and then applying <modus ponens rule>. Together they express both directions, with no extra arbitrary assumption retained after introduction.
Back to article page
