theorem eqmeq23d (G: wff) (a b c d n: nat): $ G -> a = b $ > $ G -> c = d $ > $ G -> (mod(n): a = c <-> mod(n): b = d) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqidd | G -> n = n |
|
2 | hyp h1 | G -> a = b |
|
3 | hyp h2 | G -> c = d |
|
4 | 1, 2, 3 | eqmeqd | G -> (mod(n): a = c <-> mod(n): b = d) |