∀a,b,c:ℤ.  (gcd(gcd(a;b);c) ~ gcd(a;gcd(b;c)))
{ Auto }
1. a : ℤ
2. b : ℤ
3. c : ℤ
⊢ gcd(gcd(a;b);c) ~ gcd(a;gcd(b;c))