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