Theorem addcomli 8259

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 8258	. 2 ⊢ (𝐵 + 𝐴) = (𝐴 + 𝐵)
4		addcomli.2	. 2 ⊢ (𝐴 + 𝐵) = 𝐶
5	3, 4	eqtri 2230	1 ⊢ (𝐵 + 𝐴) = 𝐶

Syntax hints:   = wceq 1375   ∈ wcel 2180  (class class class)co 5974  ℂcc 7965   + caddc 7970

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 1473  ax-gen 1475  ax-4 1536  ax-17 1552  ax-ext 2191  ax-addcom 8067

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

This theorem is referenced by:  negsubdi2i  8400  1p2e3  9213  peano2z  9450  4t4e16  9644  6t3e18  9650  6t5e30  9652  7t3e21  9655  7t4e28  9656  7t6e42  9658  7t7e49  9659  8t3e24  9661  8t4e32  9662  8t5e40  9663  8t8e64  9666  9t3e27  9668  9t4e36  9669  9t5e45  9670  9t6e54  9671  9t7e63  9672  9t8e72  9673  9t9e81  9674  4bc3eq4  10962  n2dvdsm1  12390  bitsfzo  12432  6gcd4e2  12482  gcdi  12909  2exp8  12924  2exp16  12926  eulerid  15441  cosq23lt0  15472  binom4  15618  lgsdir2lem1  15672  m1lgs  15729  2lgsoddprmlem3d  15754  ex-exp  16001  ex-bc  16003  ex-gcd  16005