theorem eqtrd (G: wff) (a b c: nat): $ G -> a = b $ > $ G -> b = c $ > $ G -> a = c $;
a = b -> b = c -> a = c
G -> a = b
G -> b = c
G -> a = c