= Solution
Use reflexivity to obtain $T_1=T_1$. In <equality elimination rule>, take $\phi(z)$ to be $z=T_1$, and replace the designated first occurrence of $T_1$ using the premise $T_1=T_2$:
\Table[
|| Line
|| Open assumptions
|| Formula
|| Justification
| 1
| 1
| $T_1=T_2$
| Premise
| 2
| 1
| $T_1=T_1$
| <equality introduction rule>
| 3
| 1
| $T_2=T_1$
| <equality elimination rule> 1, 2
]
{title=Symmetry from reflexivity and replacement}
Therefore
$$
\boxed{T_2=T_1.}
$$
The second occurrence of $T_1$ in $T_1=T_1$ is part of the fixed parameter in $\phi(z)$ and is not replaced.
Back to article page
