Metamath Proof Explorer

Theorem gcd32

Description: Swap the second and third arguments of a gcd. (Contributed by Scott Fenton, 8-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion gcd32 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A gcd B gcd C = A gcd C gcd B

Proof

Step Hyp Ref Expression
1 gcdcom ⊢ B ∈ ℤ ∧ C ∈ ℤ → B gcd C = C gcd B
2 1 3adant1 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → B gcd C = C gcd B
3 2 oveq2d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A gcd B gcd C = A gcd C gcd B
4 gcdass ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A gcd B gcd C = A gcd B gcd C
5 gcdass ⊢ A ∈ ℤ ∧ C ∈ ℤ ∧ B ∈ ℤ → A gcd C gcd B = A gcd C gcd B
6 5 3com23 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A gcd C gcd B = A gcd C gcd B
7 3 4 6 3eqtr4d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A gcd B gcd C = A gcd C gcd B