Theorem eqtr3 ≪ | index | src | ≫

theorem eqtr3 (a b c: nat): $ b = a -> b = c -> a = c $;

b = a -> b = c -> a = c

Axiom use