Theorem addcomli 8043

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

Syntax hints:   = wceq 1343   e. wcel 2136  (class class class)co 5842   CCcc 7751   + caddc 7756

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147  ax-addcom 7853

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

This theorem is referenced by:  negsubdi2i  8184  1p2e3  8991  peano2z  9227  4t4e16  9420  6t3e18  9426  6t5e30  9428  7t3e21  9431  7t4e28  9432  7t6e42  9434  7t7e49  9435  8t3e24  9437  8t4e32  9438  8t5e40  9439  8t8e64  9442  9t3e27  9444  9t4e36  9445  9t5e45  9446  9t6e54  9447  9t7e63  9448  9t8e72  9449  9t9e81  9450  4bc3eq4  10686  n2dvdsm1  11850  6gcd4e2  11928  eulerid  13363  cosq23lt0  13394  binom4  13537  lgsdir2lem1  13569  ex-exp  13608  ex-bc  13610  ex-gcd  13612