Theorem addcomli 7931

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

Syntax hints:   = wceq 1332   ∈ wcel 1481  (class class class)co 5782  ℂcc 7642   + caddc 7647

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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122  ax-addcom 7744

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

This theorem is referenced by:  negsubdi2i  8072  1p2e3  8878  peano2z  9114  4t4e16  9304  6t3e18  9310  6t5e30  9312  7t3e21  9315  7t4e28  9316  7t6e42  9318  7t7e49  9319  8t3e24  9321  8t4e32  9322  8t5e40  9323  8t8e64  9326  9t3e27  9328  9t4e36  9329  9t5e45  9330  9t6e54  9331  9t7e63  9332  9t8e72  9333  9t9e81  9334  4bc3eq4  10551  n2dvdsm1  11646  6gcd4e2  11719  eulerid  12931  cosq23lt0  12962  ex-exp  13110  ex-bc  13112  ex-gcd  13114