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∈ℤ→AgcdBgcdC=AgcdCgcdB

Proof

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