Theorem addcomli 8366

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

Hypotheses

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

Assertion

Ref	Expression
addcomli	|- ( B + A ) = C

Proof of Theorem addcomli

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

Syntax hints:   = wceq 1398   e. wcel 2202  (class class class)co 6028   CCcc 8073   + caddc 8078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213  ax-addcom 8175

This theorem depends on definitions:  df-bi 117  df-cleq 2224

This theorem is referenced by:  negsubdi2i  8507  1p2e3  9320  peano2z  9559  4t4e16  9753  6t3e18  9759  6t5e30  9761  7t3e21  9764  7t4e28  9765  7t6e42  9767  7t7e49  9768  8t3e24  9770  8t4e32  9771  8t5e40  9772  8t8e64  9775  9t3e27  9777  9t4e36  9778  9t5e45  9779  9t6e54  9780  9t7e63  9781  9t8e72  9782  9t9e81  9783  4bc3eq4  11081  n2dvdsm1  12537  bitsfzo  12579  6gcd4e2  12629  gcdi  13056  2exp8  13071  2exp16  13073  eulerid  15596  cosq23lt0  15627  binom4  15773  lgsdir2lem1  15830  m1lgs  15887  2lgsoddprmlem3d  15912  ex-exp  16424  ex-bc  16426  ex-gcd  16428