a,b:
. gcd(a;b) ~ gcd(b;a)a,b:. 
y:. GCD(a;b;y) & gcd(a;b) = ya,b,y1,y2:. GCD(a;b;y1) 
GCD(a;b;y2) (y1 ~ y2)a,b,y:. GCD(a;b;y) GCD(b;a;y)| Rank | Theorem | Name |
| 4 | a,b:. gcd(a;b) ~ gcd(b;a) | [gcd_sym] |
| cites the following: | ||
| 3 | a,b:. y:. GCD(a;b;y) & gcd(a;b) = y | [gcd_elim] |
| 0 | a,b,y1,y2:. GCD(a;b;y1) GCD(a;b;y2) (y1 ~ y2) | [gcd_unique] |
| 0 | a,b,y:. GCD(a;b;y) GCD(b;a;y) | [gcd_p_sym] |