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	⊢ ( 𝐵 + 𝐴 ) = 𝐶