Theorem addcomli 8171

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 8170	. 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 5922   CCcc 7877   + caddc 7882

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 7979

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

This theorem is referenced by:  negsubdi2i  8312  1p2e3  9125  peano2z  9362  4t4e16  9555  6t3e18  9561  6t5e30  9563  7t3e21  9566  7t4e28  9567  7t6e42  9569  7t7e49  9570  8t3e24  9572  8t4e32  9573  8t5e40  9574  8t8e64  9577  9t3e27  9579  9t4e36  9580  9t5e45  9581  9t6e54  9582  9t7e63  9583  9t8e72  9584  9t9e81  9585  4bc3eq4  10865  n2dvdsm1  12078  bitsfzo  12119  6gcd4e2  12162  gcdi  12589  2exp8  12604  2exp16  12606  eulerid  15038  cosq23lt0  15069  binom4  15215  lgsdir2lem1  15269  m1lgs  15326  2lgsoddprmlem3d  15351  ex-exp  15373  ex-bc  15375  ex-gcd  15377