Theorem equtrr

A transitive law for equality. Lemma L17 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 23-Aug-1993.)

Conclusion

\( \vdash x' = y' \rightarrow z' = x' \rightarrow z' = y' \)

Proof

equtr

com12 _