r:
, s:{s':| CoPrime(r,s') }, a,b:
.
Thm*
x:. ((x = a mod r) & (x = b mod s))r:, s:{s':| CoPrime(r,s') }. x:. ((x = 1 mod r) & (x = 0 mod s))a,b,y:. GCD(a;b;y) 
GCD(b;a;y)m,a,b:. a = b (a = b mod m)| Rank | Theorem | Name |
| 9 | r:, s:{s':| CoPrime(r,s') }, a,b:.
Thm* x:. ((x = a mod r) & (x = b mod s)) | [chrem_exists_a] |
| cites the following: | ||
| 8 | r:, s:{s':| CoPrime(r,s') }. x:. ((x = 1 mod r) & (x = 0 mod s)) | [chrem_exists_aux_a] |
| 0 | a,b,y:. GCD(a;b;y) GCD(b;a;y) | [gcd_p_sym] |
| 1 | m,a,b:. a = b (a = b mod m) | [eqmod_weakening] |