Theorem gcdcomd

Description: The gcd operator is commutative, deduction version. (Contributed by SN, 24-Aug-2024)

	Ref	Expression
Hypotheses	gcdcomd.m	$$⊢\phi \to M\in \mathbb{Z}$$
	gcdcomd.n	$$⊢\phi \to N\in \mathbb{Z}$$
Assertion	gcdcomd	$$⊢\phi \to M\gcd N=N\gcd M$$

Proof

Step	Hyp	Ref	Expression
1		gcdcomd.m	$$⊢\phi \to M\in \mathbb{Z}$$
2		gcdcomd.n	$$⊢\phi \to N\in \mathbb{Z}$$
3		gcdcom	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to M\gcd N=N\gcd M$$
4	1 2 3	syl2anc	$$⊢\phi \to M\gcd N=N\gcd M$$