Theorem equequ1

An equivalence law for equality. (Contributed by NM, 1-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Dec-2017.)

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