A simple inference in rewriting theory
The relation $\overset{*}{\leftrightarrow}$ is defined as $(\leftrightarrow)^*$, the reflexive-transitive closure of $\leftrightarrow$, and $\leftrightarrow$ is defined as $\leftarrow \cup \rightarrow$, the symmetric closure of $\rightarrow$.  This means that $\overset{*}{\leftrightarrow}$ is: a sequence of rewrites going in either direction.

Now the inference is immediate: a sequence of reverse rewrites followed by a sequence of direct rewrites is indeed a sequence of (either direction) rewrites.

Another way to view it, is that $a \rightarrow b$ stands for $a = b$ in some semantical sense, but $b$ is somewhat simpler than $a$. The relation $\overset{*}{\leftrightarrow}$ is then simply the underlying, semantical, equality.