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 -> x = z )
Assertion	sbeqal2i	|- z = y

Proof

Step	Hyp	Ref	Expression
1		sbeqal1i.1	|- ( x = y -> x = z )
2	1	sbeqal1i	|- y = z
3	2	eqcomi	|- z = y