In definition 1.3.1 of Johnstone's Sketches of an Elephant are given axioms and rules for first order logic. I recall the ones I need for the question:
(a) The structural rules consist of the identity axiom
$$ (\phi \vdash_{\vec x} \phi), $$
the substitution rule
$$ \begin{array}{cc} (\phi \vdash_{\vec x} \psi)\\ \hline (\phi[\vec s/ \vec x] \vdash_{\vec y} \psi[\vec s / \vec x]) \end{array} $$
where $\vec y$ is a string of variable including all the variables occurring in the string of terms $\vec s$, and the cut rule
$$ \begin{array}{cc} (\phi \vdash_{\vec x} \psi)\ (\psi \vdash_{\vec x} \chi)\\ \hline (\phi \vdash_{\vec x} \chi)) \end{array} $$
(b) The equality rules consist of the axioms
$$ \bigl(\top \vdash_{\vec x} (x = x)\bigr) $$
and
$$ \bigl((\vec x = \vec y \wedge \phi) \vdash_{\vec z} \phi[\vec y/\vec x]\bigr) $$
where $\vec x$ and $\vec y$ are contexts of the same length and type, $(\vec x = \vec y)$ is a shorthand for $\bigl((x_1 =y_1) \wedge \dots \wedge(x_n = y_n)\bigr)$ and $\vec z$ is any context containing $\vec x, \vec y$ and $\text{FV}(\phi)$.
(c) The rules for (finite) conjunction are the axioms
$$ (\phi \vdash_{\vec x} \top), \quad ((\phi_1 \wedge \phi_2 \vdash_{\vec x} \phi_i)\quad (i=1, 2) $$
and the rule
$$ \begin{array}{cc} (\phi \vdash_{\vec x} \psi)\ (\phi \vdash_{\vec x} \chi)\\ \hline (\phi \vdash_{\vec x} \psi \wedge \chi) \end{array} $$
It is said it is a standard exercise to derive the sequents
$$ \bigl((x = y) \vdash_{x, y} (y=x)\bigr), \quad \bigl((x=y)\wedge (y=z) \vdash_{x, y, z} (x = z)\bigr) $$
and I can derive the second from the first, but I'm not able to derive the first one. I was told that actually the second equality axiom should rather be
$$ \bigl((\vec x = \vec y \wedge \phi[\vec x / \vec u]) \vdash_{\vec z} \phi[\vec y/\vec u]\bigr) $$
Is the latter one the right axiom and/or can it be derived? How to derive the simmetry axiom for equality?
From a categorical point of view (using completeness) it is trivial to see that they hold, but I would prefer a proof using sequent calculus.