Theorem addcomli

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

	Ref	Expression
Hypotheses	mul.1	|- A e. CC
	mul.2	|- B e. CC
	addcomli.2	|- ( A + B ) = C
Assertion	addcomli	|- ( B + A ) = C

Proof

Step	Hyp	Ref	Expression
1		mul.1	|- A e. CC
2		mul.2	|- B e. CC
3		addcomli.2	|- ( A + B ) = C
4	2 1	addcomi	|- ( B + A ) = ( A + B )
5	4 3	eqtri	|- ( B + A ) = C