Theorem addcomli 8302

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 8301	. 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 6007   CCcc 8008   + caddc 8013

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 8110

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

This theorem is referenced by:  negsubdi2i  8443  1p2e3  9256  peano2z  9493  4t4e16  9687  6t3e18  9693  6t5e30  9695  7t3e21  9698  7t4e28  9699  7t6e42  9701  7t7e49  9702  8t3e24  9704  8t4e32  9705  8t5e40  9706  8t8e64  9709  9t3e27  9711  9t4e36  9712  9t5e45  9713  9t6e54  9714  9t7e63  9715  9t8e72  9716  9t9e81  9717  4bc3eq4  11007  n2dvdsm1  12439  bitsfzo  12481  6gcd4e2  12531  gcdi  12958  2exp8  12973  2exp16  12975  eulerid  15491  cosq23lt0  15522  binom4  15668  lgsdir2lem1  15722  m1lgs  15779  2lgsoddprmlem3d  15804  ex-exp  16146  ex-bc  16148  ex-gcd  16150