Theorem addcomli 8020

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

Syntax hints:   = wceq 1335   ∈ wcel 2128  (class class class)co 5824  ℂcc 7730   + caddc 7735

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ext 2139  ax-addcom 7832

This theorem depends on definitions:  df-bi 116  df-cleq 2150

This theorem is referenced by:  negsubdi2i  8161  1p2e3  8967  peano2z  9203  4t4e16  9393  6t3e18  9399  6t5e30  9401  7t3e21  9404  7t4e28  9405  7t6e42  9407  7t7e49  9408  8t3e24  9410  8t4e32  9411  8t5e40  9412  8t8e64  9415  9t3e27  9417  9t4e36  9418  9t5e45  9419  9t6e54  9420  9t7e63  9421  9t8e72  9422  9t9e81  9423  4bc3eq4  10647  n2dvdsm1  11804  6gcd4e2  11879  eulerid  13134  cosq23lt0  13165  binom4  13307  ex-exp  13314  ex-bc  13316  ex-gcd  13318