Theorem addcomli 8418

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

Syntax hints:   = wceq 1398   e. wcel 2203  (class class class)co 6050   CCcc 8125   + caddc 8130

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 2214  ax-addcom 8227

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

This theorem is referenced by:  negsubdi2i  8559  1p2e3  9372  peano2z  9613  4t4e16  9807  6t3e18  9813  6t5e30  9815  7t3e21  9818  7t4e28  9819  7t6e42  9821  7t7e49  9822  8t3e24  9824  8t4e32  9825  8t5e40  9826  8t8e64  9829  9t3e27  9831  9t4e36  9832  9t5e45  9833  9t6e54  9834  9t7e63  9835  9t8e72  9836  9t9e81  9837  4bc3eq4  11136  n2dvdsm1  12599  bitsfzo  12641  6gcd4e2  12691  gcdi  13118  2exp8  13133  2exp16  13135  eulerid  15667  cosq23lt0  15698  binom4  15844  lgsdir2lem1  15901  m1lgs  15958  2lgsoddprmlem3d  15983  ex-exp  16495  ex-bc  16497  ex-gcd  16499