Metamath Proof Explorer

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 
|- ( x = y -> ( z = x -> z = y ) )

Proof

Step Hyp Ref Expression
1 equtr 
 |-  ( z = x -> ( x = y -> z = y ) )
2 1 com12 
 |-  ( x = y -> ( z = x -> z = y ) )