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