theorem zeqmcomd (G: wff) (a b n: nat): $ G -> modZ(n): a = b $ > $ G -> modZ(n): b = a $;
modZ(n): a = b -> modZ(n): b = a
G -> modZ(n): a = b
G -> modZ(n): b = a