Theorem addcomli 8188

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

Syntax hints:   = wceq 1364   e. wcel 2167  (class class class)co 5925   CCcc 7894   + caddc 7899

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178  ax-addcom 7996

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

This theorem is referenced by:  negsubdi2i  8329  1p2e3  9142  peano2z  9379  4t4e16  9572  6t3e18  9578  6t5e30  9580  7t3e21  9583  7t4e28  9584  7t6e42  9586  7t7e49  9587  8t3e24  9589  8t4e32  9590  8t5e40  9591  8t8e64  9594  9t3e27  9596  9t4e36  9597  9t5e45  9598  9t6e54  9599  9t7e63  9600  9t8e72  9601  9t9e81  9602  4bc3eq4  10882  n2dvdsm1  12095  bitsfzo  12137  6gcd4e2  12187  gcdi  12614  2exp8  12629  2exp16  12631  eulerid  15122  cosq23lt0  15153  binom4  15299  lgsdir2lem1  15353  m1lgs  15410  2lgsoddprmlem3d  15435  ex-exp  15457  ex-bc  15459  ex-gcd  15461