MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-8d Unicode version

Axiom ax-8d 2235
Description: Distinct varable version of ax-8 1643. (Contributed by Mario Carneiro, 14-Aug-2015.)
Assertion
Ref Expression
ax-8d  |-  ( x  =  y  ->  (
x  =  z  -> 
y  =  z ) )
Distinct variable group:    x, y, z

Detailed syntax breakdown of Axiom ax-8d
StepHypRef Expression
1 vx . . 3  set  x
2 vy . . 3  set  y
31, 2weq 1624 . 2  wff  x  =  y
4 vz . . . 4  set  z
51, 4weq 1624 . . 3  wff  x  =  z
62, 4weq 1624 . . 3  wff  y  =  z
75, 6wi 4 . 2  wff  ( x  =  z  ->  y  =  z )
83, 7wi 4 1  wff  ( x  =  y  ->  (
x  =  z  -> 
y  =  z ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator