Theorem sbeqal2i

Description: If x = y implies x = z , then we can infer z = y . (Contributed by Andrew Salmon, 3-Jun-2011)

	Ref	Expression
Hypothesis	sbeqal1i.1	$$⊢x=y\to x=z$$
Assertion	sbeqal2i	$$⊢z=y$$

Proof

Step	Hyp	Ref	Expression
1		sbeqal1i.1	$$⊢x=y\to x=z$$
2	1	sbeqal1i	$$⊢y=z$$
3	2	eqcomi	$$⊢z=y$$