Metamath Proof Explorer


Theorem mulcomnni

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

Ref Expression
Hypotheses mulcomnni.1 A
mulcomnni.2 B
Assertion mulcomnni A B = B A

Proof

Step Hyp Ref Expression
1 mulcomnni.1 A
2 mulcomnni.2 B
3 1 nncni A
4 2 nncni B
5 3 4 mulcomi A B = B A