Theorem addcomli 8323

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

Syntax hints:   = wceq 1397   e. wcel 2202  (class class class)co 6017   CCcc 8029   + caddc 8034

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213  ax-addcom 8131

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

This theorem is referenced by:  negsubdi2i  8464  1p2e3  9277  peano2z  9514  4t4e16  9708  6t3e18  9714  6t5e30  9716  7t3e21  9719  7t4e28  9720  7t6e42  9722  7t7e49  9723  8t3e24  9725  8t4e32  9726  8t5e40  9727  8t8e64  9730  9t3e27  9732  9t4e36  9733  9t5e45  9734  9t6e54  9735  9t7e63  9736  9t8e72  9737  9t9e81  9738  4bc3eq4  11034  n2dvdsm1  12473  bitsfzo  12515  6gcd4e2  12565  gcdi  12992  2exp8  13007  2exp16  13009  eulerid  15525  cosq23lt0  15556  binom4  15702  lgsdir2lem1  15756  m1lgs  15813  2lgsoddprmlem3d  15838  ex-exp  16323  ex-bc  16325  ex-gcd  16327