Theorem addcomli 8237

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

Syntax hints:   = wceq 1373   e. wcel 2177  (class class class)co 5957   CCcc 7943   + caddc 7948

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188  ax-addcom 8045

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

This theorem is referenced by:  negsubdi2i  8378  1p2e3  9191  peano2z  9428  4t4e16  9622  6t3e18  9628  6t5e30  9630  7t3e21  9633  7t4e28  9634  7t6e42  9636  7t7e49  9637  8t3e24  9639  8t4e32  9640  8t5e40  9641  8t8e64  9644  9t3e27  9646  9t4e36  9647  9t5e45  9648  9t6e54  9649  9t7e63  9650  9t8e72  9651  9t9e81  9652  4bc3eq4  10940  n2dvdsm1  12299  bitsfzo  12341  6gcd4e2  12391  gcdi  12818  2exp8  12833  2exp16  12835  eulerid  15349  cosq23lt0  15380  binom4  15526  lgsdir2lem1  15580  m1lgs  15637  2lgsoddprmlem3d  15662  ex-exp  15802  ex-bc  15804  ex-gcd  15806