Metamath Proof Explorer


Theorem gcdcomd

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

Ref Expression
Hypotheses gcdcomd.m
|- ( ph -> M e. ZZ )
gcdcomd.n
|- ( ph -> N e. ZZ )
Assertion gcdcomd
|- ( ph -> ( M gcd N ) = ( N gcd M ) )

Proof

Step Hyp Ref Expression
1 gcdcomd.m
 |-  ( ph -> M e. ZZ )
2 gcdcomd.n
 |-  ( ph -> N e. ZZ )
3 gcdcom
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) = ( N gcd M ) )
4 1 2 3 syl2anc
 |-  ( ph -> ( M gcd N ) = ( N gcd M ) )