Theorem equsb3rOLD

Description: Obsolete version of equsb3r as of 2-Sep-2023. (Contributed by AV, 29-Jul-2023) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	equsb3rOLD	$$⊢\left[y/x\right]z=x\leftrightarrow z=y$$

Proof

Step	Hyp	Ref	Expression
1		equcom	$$⊢z=x\leftrightarrow x=z$$
2	1	sbbii	$$⊢\left[y/x\right]z=x\leftrightarrow \left[y/x\right]x=z$$
3		equsb3	$$⊢\left[y/x\right]x=z\leftrightarrow y=z$$
4		equcom	$$⊢y=z\leftrightarrow z=y$$
5	2 3 4	3bitri	$$⊢\left[y/x\right]z=x\leftrightarrow z=y$$