Theorem addcomli 8064

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

Syntax hints:   = wceq 1348   e. wcel 2141  (class class class)co 5853   CCcc 7772   + caddc 7777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152  ax-addcom 7874

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  negsubdi2i  8205  1p2e3  9012  peano2z  9248  4t4e16  9441  6t3e18  9447  6t5e30  9449  7t3e21  9452  7t4e28  9453  7t6e42  9455  7t7e49  9456  8t3e24  9458  8t4e32  9459  8t5e40  9460  8t8e64  9463  9t3e27  9465  9t4e36  9466  9t5e45  9467  9t6e54  9468  9t7e63  9469  9t8e72  9470  9t9e81  9471  4bc3eq4  10707  n2dvdsm1  11872  6gcd4e2  11950  eulerid  13517  cosq23lt0  13548  binom4  13691  lgsdir2lem1  13723  ex-exp  13762  ex-bc  13764  ex-gcd  13766