Identity elimination 1

By identity elimination (substitution of identicals), if $t$ and $t^{\prime }$ are terms, from $t=t^{\prime }$ and $\varphi (x/t)$, we may derive $\varphi (x/t^{\prime })$ (we substitute $t$ for $t^{\prime }$ since they are identical):

$$\frac{t=t^{\prime },\varphi (x/t)}{\varphi (x/t^{\prime })}(\text{IE})$$