Theorem addcomli 8317

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

Syntax hints:   = wceq 1395   ∈ wcel 2200  (class class class)co 6013  ℂcc 8023   + caddc 8028

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 8125

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

This theorem is referenced by:  negsubdi2i  8458  1p2e3  9271  peano2z  9508  4t4e16  9702  6t3e18  9708  6t5e30  9710  7t3e21  9713  7t4e28  9714  7t6e42  9716  7t7e49  9717  8t3e24  9719  8t4e32  9720  8t5e40  9721  8t8e64  9724  9t3e27  9726  9t4e36  9727  9t5e45  9728  9t6e54  9729  9t7e63  9730  9t8e72  9731  9t9e81  9732  4bc3eq4  11028  n2dvdsm1  12467  bitsfzo  12509  6gcd4e2  12559  gcdi  12986  2exp8  13001  2exp16  13003  eulerid  15519  cosq23lt0  15550  binom4  15696  lgsdir2lem1  15750  m1lgs  15807  2lgsoddprmlem3d  15832  ex-exp  16273  ex-bc  16275  ex-gcd  16277