m,a,b,c:
. (a = b mod m) 
(b = c mod m) (a = c mod m)a,b1,b2:. a | b1 a | b2 a | b1+b2| Theorem | Name |
| m,a,b,c:. (a = b mod m) (b = c mod m) (a = c mod m) | [eqmod_transitivity] |
| cites the following: | |
| a,b1,b2:. a | b1 a | b2 a | b1+b2 | [divisor_of_sum] |