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