Theorem equsb3

Substitution in an equality. (Contributed by Raph Levien and FL, 4-Dec-2005.) Reduce axiom usage. (Revised by Wolf Lammen, 23-Jul-2023.)

Conclusion
\( \vdash [ y' / x ] \, x = z' \leftrightarrow y' = z' \)
Proof
l0
equequ1
\( \vdash x = w \rightarrow (x = z' \leftrightarrow w = z') \)
equequ1
\( \vdash w = y' \rightarrow (w = z' \leftrightarrow y' = z') \)
sbievw2 l0 _