Metamath Proof Explorer


Theorem addcomli

Description: Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015)

Ref Expression
Hypotheses mul.1 𝐴 ∈ ℂ
mul.2 𝐵 ∈ ℂ
addcomli.2 ( 𝐴 + 𝐵 ) = 𝐶
Assertion addcomli ( 𝐵 + 𝐴 ) = 𝐶

Proof

Step Hyp Ref Expression
1 mul.1 𝐴 ∈ ℂ
2 mul.2 𝐵 ∈ ℂ
3 addcomli.2 ( 𝐴 + 𝐵 ) = 𝐶
4 2 1 addcomi ( 𝐵 + 𝐴 ) = ( 𝐴 + 𝐵 )
5 4 3 eqtri ( 𝐵 + 𝐴 ) = 𝐶