= Solution
For transitivity of <first-order equality>, take the substitution formula $\phi(u)\equiv(T_1=u)$:
``
1 T₁ = T₂ premise
2 T₂ = T₃ premise
3 T₁ = T₃ =-elim 2,1; φ(u) := (T₁ = u)
``
For symmetry, use reflexivity and $\psi(u)\equiv(u=T_1)$:
``
1 T₁ = T₂ premise
2 T₁ = T₁ =-intro
3 T₂ = T₁ =-elim 1,2; ψ(u) := (u = T₁)
``
Thus \b[both transitivity and symmetry follow from the two equality rules]. In the symmetry proof, only the designated first occurrence in $T_1=T_1$ is replaced; the second remains fixed.
Back to article page
