Assume we have the following statement:
$$\mathsf{K} + \mathsf{A4} + \mathsf{AB} \models \mathsf{A5},$$
where $\mathsf{A4}$ is the transitivity axiom, and $\mathsf{AB}$ is the symmetry axiom. One can show that this relation holds considering required frames or building canonical models. In the former case our reasoning could be as follows: "if there are two arrows from $x$ to $y$ and $z$ then due to symmetry $y\to x$ and from transitivity $y\to z$ qed". We can even write this as a first order formula. I wonder if we can derive $\mathsf{A5}$ from the left hand side logic somehow, for example, convert our reasoning or a first order formula into the derivation. I didn't see the answer anywhere, however I haven't looked for it in every source I have. Can someone help me?
$\lozenge \varphi \rightarrow \square \lozenge \lozenge \varphi$ (contraposition of AB with $\lozenge \varphi$)
$\lozenge \lozenge \varphi \rightarrow \lozenge \varphi$ (contraposition of A4)
$\square (\lozenge \lozenge \varphi \rightarrow \lozenge \varphi)$ (necessitation of 3)
$\square (\lozenge \lozenge \varphi \rightarrow \lozenge \varphi) \rightarrow (\square \lozenge \lozenge \varphi \rightarrow \square \lozenge \varphi)$ (K)
$\square \lozenge \lozenge \varphi \rightarrow \square \lozenge \varphi$ (modus ponens 3 and 4)
$(\lozenge \varphi \rightarrow \square \lozenge \lozenge \varphi) \wedge (\square \lozenge \lozenge \varphi \rightarrow \square \lozenge \varphi) \rightarrow (\lozenge \varphi \rightarrow \square \lozenge \varphi)$ (propositional reasoning)
$\lozenge \varphi \rightarrow \square \lozenge \varphi$ (modus ponens 1,5, and 6)