m,a,a',b,b':
.
Thm* (a = a' mod m)
(b = b' mod m) ((a = b mod m) 
(a' = b' mod m))m,a,b:. (a = b mod m) (b = a mod m)m,a,b,c:. (a = b mod m) (b = c mod m) (a = c mod m)| Rank | Theorem | Name |
| 2 | m,a,a',b,b':.
Thm* (a = a' mod m) (b = b' mod m) ((a = b mod m) (a' = b' mod m)) | [eqmod_fun] |
| cites the following: | ||
| 1 | m,a,b:. (a = b mod m) (b = a mod m) | [eqmod_inversion] |
| 1 | m,a,b,c:. (a = b mod m) (b = c mod m) (a = c mod m) | [eqmod_transitivity] |