Axiom ax-8d

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

	Ref	Expression
Assertion	ax-8d	$$⊢x=y\to \left(x=z\to y=z\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1	0	cv	$$setvarx$$
2		vy	$$setvary$$
3	2	cv	$$setvary$$
4	1 3	wceq	$$wffx=y$$
5		vz	$$setvarz$$
6	5	cv	$$setvarz$$
7	1 6	wceq	$$wffx=z$$
8	3 6	wceq	$$wffy=z$$
9	7 8	wi	$$wff\left(x=z\to y=z\right)$$
10	4 9	wi	$$wff\left(x=y\to \left(x=z\to y=z\right)\right)$$