Theorem addcomli 8465

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

Syntax hints:   = wceq 1402   ∈ wcel 2209  (class class class)co 6079  ℂcc 8171   + caddc 8176

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220  ax-addcom 8273

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

This theorem is referenced by:  negsubdi2i  8606  1p2e3  9422  peano2z  9663  4t4e16  9858  6t3e18  9864  6t5e30  9866  7t3e21  9869  7t4e28  9870  7t6e42  9872  7t7e49  9873  8t3e24  9875  8t4e32  9876  8t5e40  9877  8t8e64  9880  9t3e27  9882  9t4e36  9883  9t5e45  9884  9t6e54  9885  9t7e63  9886  9t8e72  9887  9t9e81  9888  4bc3eq4  11195  n2dvdsm1  12663  bitsfzo  12705  6gcd4e2  12755  gcdi  13182  2exp8  13197  2exp16  13199  eulerid  15886  cosq23lt0  15917  binom4  16064  log2ublem3  16068  log2ublog2  16069  lgsdir2lem1  16130  m1lgs  16187  2lgsoddprmlem3d  16212  ex-exp  16724  ex-bc  16726  ex-gcd  16728