Theorem addcomli 8314

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

Syntax hints:   = wceq 1395   e. wcel 2200  (class class class)co 6013   CCcc 8020   + caddc 8025

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211  ax-addcom 8122

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

This theorem is referenced by:  negsubdi2i  8455  1p2e3  9268  peano2z  9505  4t4e16  9699  6t3e18  9705  6t5e30  9707  7t3e21  9710  7t4e28  9711  7t6e42  9713  7t7e49  9714  8t3e24  9716  8t4e32  9717  8t5e40  9718  8t8e64  9721  9t3e27  9723  9t4e36  9724  9t5e45  9725  9t6e54  9726  9t7e63  9727  9t8e72  9728  9t9e81  9729  4bc3eq4  11025  n2dvdsm1  12464  bitsfzo  12506  6gcd4e2  12556  gcdi  12983  2exp8  12998  2exp16  13000  eulerid  15516  cosq23lt0  15547  binom4  15693  lgsdir2lem1  15747  m1lgs  15804  2lgsoddprmlem3d  15829  ex-exp  16259  ex-bc  16261  ex-gcd  16263