Theorem addcomli 8471

Description: Addition is commutative. (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 8470	. 2 ⊢ (𝐵 + 𝐴) = (𝐴 + 𝐵)
4		addcomli.2	. 2 ⊢ (𝐴 + 𝐵) = 𝐶
5	3, 4	eqtri 2259	1 ⊢ (𝐵 + 𝐴) = 𝐶

This proof depends on syntax axioms:   = wceq 1402   ∈ wcel 2209  (class class class)co 6085  ℂcc 8177   + caddc 8182

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 8279

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

This theorem is used by:  negsubdi2i  8612  1p2e3  9440  peano2z  9682  4t4e16  9877  6t3e18  9883  6t5e30  9885  7t3e21  9888  7t4e28  9889  7t6e42  9891  7t7e49  9892  8t3e24  9894  8t4e32  9895  8t5e40  9896  8t8e64  9899  9t3e27  9901  9t4e36  9902  9t5e45  9903  9t6e54  9904  9t7e63  9905  9t8e72  9906  9t9e81  9907  4bc3eq4  11214  n2dvdsm1  12682  bitsfzo  12724  6gcd4e2  12774  gcdi  13201  2exp8  13216  2exp16  13218  eulerid  15906  cosq23lt0  15937  binom4  16087  log2ublem3  16091  log2ublog2  16092  lgsdir2lem1  16159  m1lgs  16216  2lgsoddprmlem3d  16241  ex-exp  16753  ex-bc  16755  ex-gcd  16757