Theorem addcomli 8287

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

Syntax hints:   = wceq 1395   e. wcel 2200  (class class class)co 6000   CCcc 7993   + caddc 7998

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211  ax-addcom 8095

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

This theorem is referenced by:  negsubdi2i  8428  1p2e3  9241  peano2z  9478  4t4e16  9672  6t3e18  9678  6t5e30  9680  7t3e21  9683  7t4e28  9684  7t6e42  9686  7t7e49  9687  8t3e24  9689  8t4e32  9690  8t5e40  9691  8t8e64  9694  9t3e27  9696  9t4e36  9697  9t5e45  9698  9t6e54  9699  9t7e63  9700  9t8e72  9701  9t9e81  9702  4bc3eq4  10990  n2dvdsm1  12419  bitsfzo  12461  6gcd4e2  12511  gcdi  12938  2exp8  12953  2exp16  12955  eulerid  15470  cosq23lt0  15501  binom4  15647  lgsdir2lem1  15701  m1lgs  15758  2lgsoddprmlem3d  15783  ex-exp  16049  ex-bc  16051  ex-gcd  16053