Let $r$ be a ternary relation symbol, $f$ a binary function symbol, and $x,y,z$ distinct variables. Let $F(x,y,z)$ be the formula $x=y \rightarrow (rfxyxz \rightarrow rfyxxz)$.
I need to show the $F$ is valid, by showing that in any interpretation $S$, $F^S(a,b,c)$ holds for any $a,b,c$.
So i know that if $F$ is $t_1(x)=t_2(x)$, then $F^S(a)$ holds iff $(t_1)^S(a)=(t_2)^S(a)$. And if $F$ is $rt_1(x)...t_n(x)$, then $F^S(a)$ holds iff $r^S((t_1)^S(a),...,(t_n)^S(a))$ holds. Not sure how to formally prove the formula though.