# Proving a logic formula

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.

-

(i) from $x = y$ and $\varphi(x)$ you can infer $\varphi(y)$ and (ii) from $x = y$ and $\varphi(y)$ you can infer $\varphi(x)$ (for any context $\varphi(\cdot)$).
So given $x = y$ and $Rfxyxz$ you can infer $Rfxxxz$ (put $\varphi(\cdot) = Rfx\cdot xz$ and use (ii)). And from $x = y$ and $Rfxxxz$ you can infer $Rfyxxz$ (put $\varphi(\cdot) = Rf\cdot xxz$ and use (i)).