Theorem addcomli 8174

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

Syntax hints:   = wceq 1364   e. wcel 2167  (class class class)co 5923   CCcc 7880   + caddc 7885

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178  ax-addcom 7982

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

This theorem is referenced by:  negsubdi2i  8315  1p2e3  9128  peano2z  9365  4t4e16  9558  6t3e18  9564  6t5e30  9566  7t3e21  9569  7t4e28  9570  7t6e42  9572  7t7e49  9573  8t3e24  9575  8t4e32  9576  8t5e40  9577  8t8e64  9580  9t3e27  9582  9t4e36  9583  9t5e45  9584  9t6e54  9585  9t7e63  9586  9t8e72  9587  9t9e81  9588  4bc3eq4  10868  n2dvdsm1  12081  bitsfzo  12123  6gcd4e2  12173  gcdi  12600  2exp8  12615  2exp16  12617  eulerid  15064  cosq23lt0  15095  binom4  15241  lgsdir2lem1  15295  m1lgs  15352  2lgsoddprmlem3d  15377  ex-exp  15399  ex-bc  15401  ex-gcd  15403