Theorem sbeqal1i

Description: Suppose you know x = y implies x = z , assuming x and z are distinct. Then, y = z . (Contributed by Andrew Salmon, 3-Jun-2011)

	Ref	Expression
Hypothesis	sbeqal1i.1	⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑧 )
Assertion	sbeqal1i	⊢ 𝑦 = 𝑧

Proof

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