Theorem addcomli

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

	Ref	Expression
Hypotheses	mul.1	$$⊢A\in ℂ$$
	mul.2	$$⊢B\in ℂ$$
	addcomli.2	$$⊢A+B=C$$
Assertion	addcomli	$$⊢B+A=C$$

Proof

Step	Hyp	Ref	Expression
1		mul.1	$$⊢A\in ℂ$$
2		mul.2	$$⊢B\in ℂ$$
3		addcomli.2	$$⊢A+B=C$$
4	2 1	addcomi	$$⊢B+A=A+B$$
5	4 3	eqtri	$$⊢B+A=C$$