Theorem addcomli 8417

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 8416	. 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 6049   CCcc 8124   + caddc 8129

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 8226

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

This theorem is referenced by:  negsubdi2i  8558  1p2e3  9371  peano2z  9612  4t4e16  9806  6t3e18  9812  6t5e30  9814  7t3e21  9817  7t4e28  9818  7t6e42  9820  7t7e49  9821  8t3e24  9823  8t4e32  9824  8t5e40  9825  8t8e64  9828  9t3e27  9830  9t4e36  9831  9t5e45  9832  9t6e54  9833  9t7e63  9834  9t8e72  9835  9t9e81  9836  4bc3eq4  11134  n2dvdsm1  12595  bitsfzo  12637  6gcd4e2  12687  gcdi  13114  2exp8  13129  2exp16  13131  eulerid  15659  cosq23lt0  15690  binom4  15836  lgsdir2lem1  15893  m1lgs  15950  2lgsoddprmlem3d  15975  ex-exp  16487  ex-bc  16489  ex-gcd  16491