theorem zdvdeq2d (_G: wff) (m _n1 _n2: nat): $ _G -> _n1 = _n2 $ > $ _G -> (m |Z _n1 <-> m |Z _n2) $;
_G -> m = m
_G -> _n1 = _n2
_G -> (m |Z _n1 <-> m |Z _n2)