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	⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑧 )
Assertion	sbeqal2i	⊢ 𝑧 = 𝑦

Proof

Step	Hyp	Ref	Expression
1		sbeqal1i.1	⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑧 )
2	1	sbeqal1i	⊢ 𝑦 = 𝑧
3	2	eqcomi	⊢ 𝑧 = 𝑦