Need help for a proof ( sequent calculus )

Question

I have to prove the following:

$$\vdash((A \to B) \land (B \to A)) \to (A \leftrightarrow B)$$

But I'm totally stuck here after using introduction of implication and introduction of equivalence:

\begin{align} \dfrac{\dfrac{ (A \to B) \land (B \to A), A\vdash B \qquad (A \to B) \land (B \to A), B\vdash A }{(A \to B) \land (B\to A)\vdash A \leftrightarrow B}\leftrightarrow_R}{\vdash ((A \to B) \land (B \to A)) \to (A \leftrightarrow B)}\to_R \end{align}

Answer 1

The following is a derivation in sequent calculus of the sequent $\vdash ((A \to B) \land (B \to A)) \to (A \leftrightarrow B)$.

\begin{align} \dfrac{\dfrac{ \dfrac{\dfrac{\dfrac{A \vdash A \qquad B \vdash B}{A \to B, \, A \vdash B}\to_L}{A \to B, \, B \to A, \, A \vdash B}weak_L}{(A \to B) \land (B \to A), A\vdash B}\land_L \qquad \dfrac{\dfrac{\dfrac{B \vdash B \qquad A \vdash A}{B \to A, \, B \vdash A}\to_L}{A \to B, \, B \to A, \, B\vdash A}weak_L}{(A \to B) \land (B \to A), B\vdash A}\land_L}{(A \to B) \land (B\to A)\vdash A \leftrightarrow B}\leftrightarrow_R}{\vdash ((A \to B) \land (B \to A)) \to (A \leftrightarrow B)}\to_R \end{align}

Note that in sequent calculus every inference rule (except the cut rule and the axiom) is an introduction rule. So, talking of "introduction rules" for the sequent calculus is too generic. In sequent calculus, inference rules are split into "left" (they introduce a connective on the left of $\vdash$) and "right" (they introduce a connective on the right of $\vdash$).