Metamath Proof Explorer

Axiom ax-8d

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

Ref Expression
Assertion ax-8d 
|- ( x = y -> ( x = z -> y = z ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx 
 |-  x
1 0 cv 
 |-  x
2 vy 
 |-  y
3 2 cv 
 |-  y
4 1 3 wceq 
 |-  x = y
5 vz 
 |-  z
6 5 cv 
 |-  z
7 1 6 wceq 
 |-  x = z
8 3 6 wceq 
 |-  y = z
9 7 8 wi 
 |-  ( x = z -> y = z )
10 4 9 wi 
 |-  ( x = y -> ( x = z -> y = z ) )