a,b,c:
. gcd(gcd(a;b);c) ~ gcd(a;gcd(b;c))a,b,y:. GCD(a;b;y) 
GCD(b;a;y)a,b,c,x,y:.
Thm* GCD(a;b;x)
Thm*
Thm* GCD(x;c;y)
Thm*
Thm* y | a & y | b & y | c & (
z:. z | a z | b z | c z | y)| Theorem | Name |
| a,b,c:. gcd(gcd(a;b);c) ~ gcd(a;gcd(b;c)) | [gcd_assoc] |
| cites the following: | |
| a,b,y:. GCD(a;b;y) GCD(b;a;y) | [gcd_p_sym] |
| a,b,c,x,y:.
Thm* GCD(a;b;x) Thm*
Thm* GCD(x;c;y) Thm*
Thm* y | a & y | b & y | c & ( z:. z | a z | b z | c z | y) | [gcd_of_triple] |