Metamath Proof Explorer


Theorem mulcomnni

Description: Commutative law for multiplication. (Contributed by metakunt, 25-Apr-2024)

Ref Expression
Hypotheses mulcomnni.1
|- A e. NN
mulcomnni.2
|- B e. NN
Assertion mulcomnni
|- ( A x. B ) = ( B x. A )

Proof

Step Hyp Ref Expression
1 mulcomnni.1
 |-  A e. NN
2 mulcomnni.2
 |-  B e. NN
3 1 nncni
 |-  A e. CC
4 2 nncni
 |-  B e. CC
5 3 4 mulcomi
 |-  ( A x. B ) = ( B x. A )