Metamath Proof Explorer


Theorem gcdcomd

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

Ref Expression
Hypotheses gcdcomd.m φM
gcdcomd.n φN
Assertion gcdcomd φMgcdN=NgcdM

Proof

Step Hyp Ref Expression
1 gcdcomd.m φM
2 gcdcomd.n φN
3 gcdcom MNMgcdN=NgcdM
4 1 2 3 syl2anc φMgcdN=NgcdM