This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem equtr

Description: A transitive law for equality. (Contributed by NM, 23-Aug-1993)

Ref Expression
Assertion equtr 
|- ( x = y -> ( y = z -> x = z ) )

Proof

Step Hyp Ref Expression
1 ax7 
 |-  ( y = x -> ( y = z -> x = z ) )
2 1 equcoms 
 |-  ( x = y -> ( y = z -> x = z ) )