Metamath Proof Explorer


Theorem addcomnni

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

Ref Expression
Hypotheses addcomnni.1 A
addcomnni.2 B
Assertion addcomnni A + B = B + A

Proof

Step Hyp Ref Expression
1 addcomnni.1 A
2 addcomnni.2 B
3 1 nncni A
4 2 nncni B
5 3 4 addcomi A + B = B + A