Theorem addcomli 8014

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

Syntax hints:   = wceq 1335   e. wcel 2128  (class class class)co 5821   CCcc 7724   + caddc 7729

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 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ext 2139  ax-addcom 7826

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

This theorem is referenced by:  negsubdi2i  8155  1p2e3  8961  peano2z  9197  4t4e16  9387  6t3e18  9393  6t5e30  9395  7t3e21  9398  7t4e28  9399  7t6e42  9401  7t7e49  9402  8t3e24  9404  8t4e32  9405  8t5e40  9406  8t8e64  9409  9t3e27  9411  9t4e36  9412  9t5e45  9413  9t6e54  9414  9t7e63  9415  9t8e72  9416  9t9e81  9417  4bc3eq4  10640  n2dvdsm1  11796  6gcd4e2  11870  eulerid  13094  cosq23lt0  13125  binom4  13267  ex-exp  13274  ex-bc  13276  ex-gcd  13278