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