Theorem addcomli 8329

Description: Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015.)

Hypotheses

Ref	Expression
mul.1	⊢ 𝐴 ∈ ℂ
mul.2	⊢ 𝐵 ∈ ℂ
addcomli.2	⊢ (𝐴 + 𝐵) = 𝐶

Assertion

Ref	Expression
addcomli	⊢ (𝐵 + 𝐴) = 𝐶

Proof of Theorem addcomli

Step	Hyp	Ref	Expression
1		mul.2	. . 3 ⊢ 𝐵 ∈ ℂ
2		mul.1	. . 3 ⊢ 𝐴 ∈ ℂ
3	1, 2	addcomi 8328	. 2 ⊢ (𝐵 + 𝐴) = (𝐴 + 𝐵)
4		addcomli.2	. 2 ⊢ (𝐴 + 𝐵) = 𝐶
5	3, 4	eqtri 2251	1 ⊢ (𝐵 + 𝐴) = 𝐶

Syntax hints:   = wceq 1397   ∈ wcel 2201  (class class class)co 6023  ℂcc 8035   + caddc 8040

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2212  ax-addcom 8137

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

This theorem is referenced by:  negsubdi2i  8470  1p2e3  9283  peano2z  9520  4t4e16  9714  6t3e18  9720  6t5e30  9722  7t3e21  9725  7t4e28  9726  7t6e42  9728  7t7e49  9729  8t3e24  9731  8t4e32  9732  8t5e40  9733  8t8e64  9736  9t3e27  9738  9t4e36  9739  9t5e45  9740  9t6e54  9741  9t7e63  9742  9t8e72  9743  9t9e81  9744  4bc3eq4  11041  n2dvdsm1  12497  bitsfzo  12539  6gcd4e2  12589  gcdi  13016  2exp8  13031  2exp16  13033  eulerid  15555  cosq23lt0  15586  binom4  15732  lgsdir2lem1  15786  m1lgs  15843  2lgsoddprmlem3d  15868  ex-exp  16380  ex-bc  16382  ex-gcd  16384