Theorem addcomli 7900

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 7899	. 2 |- ( B + A ) = ( A + B )
4		addcomli.2	. 2 |- ( A + B ) = C
5	3, 4	eqtri 2158	1 |- ( B + A ) = C

Syntax hints:   = wceq 1331   e. wcel 1480  (class class class)co 5767   CCcc 7611   + caddc 7616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119  ax-addcom 7713

This theorem depends on definitions:  df-bi 116  df-cleq 2130

This theorem is referenced by:  negsubdi2i  8041  1p2e3  8847  peano2z  9083  4t4e16  9273  6t3e18  9279  6t5e30  9281  7t3e21  9284  7t4e28  9285  7t6e42  9287  7t7e49  9288  8t3e24  9290  8t4e32  9291  8t5e40  9292  8t8e64  9295  9t3e27  9297  9t4e36  9298  9t5e45  9299  9t6e54  9300  9t7e63  9301  9t8e72  9302  9t9e81  9303  4bc3eq4  10512  n2dvdsm1  11599  6gcd4e2  11672  eulerid  12872  cosq23lt0  12903  ex-exp  12928  ex-bc  12930  ex-gcd  12932