Theorem equtrr

Description: A transitive law for equality. Lemma L17 in Megill p. 446 (p. 14 of the preprint). (Contributed by NM, 23-Aug-1993)

	Ref	Expression
Assertion	equtrr	⊢ ( 𝑥 = 𝑦 → ( 𝑧 = 𝑥 → 𝑧 = 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		equtr	⊢ ( 𝑧 = 𝑥 → ( 𝑥 = 𝑦 → 𝑧 = 𝑦 ) )
2	1	com12	⊢ ( 𝑥 = 𝑦 → ( 𝑧 = 𝑥 → 𝑧 = 𝑦 ) )