Axiom ax-8d

Description: Distinct variable version of ax-7 . (Contributed by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Assertion	ax-8d	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 → 𝑦 = 𝑧 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1	0	cv	⊢ 𝑥
2		vy	⊢ 𝑦
3	2	cv	⊢ 𝑦
4	1 3	wceq	⊢ 𝑥 = 𝑦
5		vz	⊢ 𝑧
6	5	cv	⊢ 𝑧
7	1 6	wceq	⊢ 𝑥 = 𝑧
8	3 6	wceq	⊢ 𝑦 = 𝑧
9	7 8	wi	⊢ ( 𝑥 = 𝑧 → 𝑦 = 𝑧 )
10	4 9	wi	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 → 𝑦 = 𝑧 ) )