Theorem addcomli 8471

Description: Addition is commutative. (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 8470	. 2 |- ( B + A ) = ( A + B )
4		addcomli.2	. 2 |- ( A + B ) = C
5	3, 4	eqtri 2259	1 |- ( B + A ) = C

This proof depends on syntax axioms:   = wceq 1402   e. wcel 2209  (class class class)co 6085   CCcc 8177   + caddc 8182

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220  ax-addcom 8279

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  negsubdi2i  8612  1p2e3  9439  peano2z  9680  4t4e16  9875  6t3e18  9881  6t5e30  9883  7t3e21  9886  7t4e28  9887  7t6e42  9889  7t7e49  9890  8t3e24  9892  8t4e32  9893  8t5e40  9894  8t8e64  9897  9t3e27  9899  9t4e36  9900  9t5e45  9901  9t6e54  9902  9t7e63  9903  9t8e72  9904  9t9e81  9905  4bc3eq4  11212  n2dvdsm1  12680  bitsfzo  12722  6gcd4e2  12772  gcdi  13199  2exp8  13214  2exp16  13216  eulerid  15903  cosq23lt0  15934  binom4  16081  log2ublem3  16085  log2ublog2  16086  lgsdir2lem1  16147  m1lgs  16204  2lgsoddprmlem3d  16229  ex-exp  16741  ex-bc  16743  ex-gcd  16745