Theorem addcomli 8478

Description: Addition is commutative. (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 8477	. 2 |- ( B + A ) = ( A + B )
4		addcomli.2	. 2 |- ( A + B ) = C
5	3, 4	eqtri 2259	1 |- ( B + A ) = C

This proof depends on syntax axioms:   = wceq 1402   e. wcel 2209  (class class class)co 6088   CCcc 8183   + caddc 8188

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220  ax-addcom 8285

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  negsubdi2i  8619  1p2e3  9448  peano2z  9691  4t4e16  9891  6t3e18  9897  6t5e30  9899  7t3e21  9902  7t4e28  9903  7t6e42  9905  7t7e49  9906  8t3e24  9908  8t4e32  9909  8t5e40  9910  8t8e64  9913  9t3e27  9915  9t4e36  9916  9t5e45  9917  9t6e54  9918  9t7e63  9919  9t8e72  9920  9t9e81  9921  4bc3eq4  11234  n2dvdsm1  12705  bitsfzo  12747  6gcd4e2  12797  gcdi  13229  2exp8  13244  2exp16  13246  37prm  13264  43prm  13265  83prm  13266  139prm  13267  163prm  13268  317prm  13269  631prm  13270  1259lem1  13271  1259lem2  13272  1259lem3  13273  1259lem4  13274  1259lem5  13275  1259prm  13276  eulerid  16029  cosq23lt0  16060  binom4  16219  log2ublem3  16223  log2ublog2  16224  lgsdir2lem1  16352  m1lgs  16409  2lgsoddprmlem3d  16434  ex-exp  16946  ex-bc  16948  ex-gcd  16950