Theorem addcomli 8166

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

Syntax hints:   = wceq 1364   ∈ wcel 2164  (class class class)co 5919  ℂcc 7872   + caddc 7877

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175  ax-addcom 7974

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

This theorem is referenced by:  negsubdi2i  8307  1p2e3  9119  peano2z  9356  4t4e16  9549  6t3e18  9555  6t5e30  9557  7t3e21  9560  7t4e28  9561  7t6e42  9563  7t7e49  9564  8t3e24  9566  8t4e32  9567  8t5e40  9568  8t8e64  9571  9t3e27  9573  9t4e36  9574  9t5e45  9575  9t6e54  9576  9t7e63  9577  9t8e72  9578  9t9e81  9579  4bc3eq4  10847  n2dvdsm1  12057  6gcd4e2  12135  eulerid  14978  cosq23lt0  15009  binom4  15152  lgsdir2lem1  15185  m1lgs  15242  2lgsoddprmlem3d  15267  ex-exp  15289  ex-bc  15291  ex-gcd  15293