Theorem equequ2

An equivalence law for equality. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2017.) (Proof shortened by BJ, 12-Apr-2021.)

Conclusion
\( \vdash x' = y' \rightarrow (z' = x' \leftrightarrow z' = y') \)
Proof
l0
equtrr
equeuclr
impbid l0 _