Theorem addcomli 8307

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

Syntax hints:   = wceq 1395   ∈ wcel 2200  (class class class)co 6010  ℂcc 8013   + caddc 8018

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211  ax-addcom 8115

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

This theorem is referenced by:  negsubdi2i  8448  1p2e3  9261  peano2z  9498  4t4e16  9692  6t3e18  9698  6t5e30  9700  7t3e21  9703  7t4e28  9704  7t6e42  9706  7t7e49  9707  8t3e24  9709  8t4e32  9710  8t5e40  9711  8t8e64  9714  9t3e27  9716  9t4e36  9717  9t5e45  9718  9t6e54  9719  9t7e63  9720  9t8e72  9721  9t9e81  9722  4bc3eq4  11012  n2dvdsm1  12445  bitsfzo  12487  6gcd4e2  12537  gcdi  12964  2exp8  12979  2exp16  12981  eulerid  15497  cosq23lt0  15528  binom4  15674  lgsdir2lem1  15728  m1lgs  15785  2lgsoddprmlem3d  15810  ex-exp  16200  ex-bc  16202  ex-gcd  16204