Theorem addcomli 7158

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

Syntax hints:   = wceq 1243   ∈ wcel 1393  (class class class)co 5512  ℂcc 6887   + caddc 6892

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022  ax-addcom 6984

This theorem depends on definitions:  df-bi 110  df-cleq 2033

This theorem is referenced by:  negsubdi2i  7297  1p2e3  8044  peano2z  8281  4t4e16  8440  6t3e18  8445  6t5e30  8447  7t3e21  8450  7t4e28  8451  7t6e42  8453  7t7e49  8454  8t3e24  8456  8t4e32  8457  8t5e40  8458  8t8e64  8461  9t3e27  8463  9t4e36  8464  9t5e45  8465  9t6e54  8466  9t7e63  8467  9t8e72  8468  9t9e81  8469