Theorem addcomli 8324

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

Syntax hints:   = wceq 1397   ∈ wcel 2202  (class class class)co 6018  ℂcc 8030   + caddc 8035

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213  ax-addcom 8132

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

This theorem is referenced by:  negsubdi2i  8465  1p2e3  9278  peano2z  9515  4t4e16  9709  6t3e18  9715  6t5e30  9717  7t3e21  9720  7t4e28  9721  7t6e42  9723  7t7e49  9724  8t3e24  9726  8t4e32  9727  8t5e40  9728  8t8e64  9731  9t3e27  9733  9t4e36  9734  9t5e45  9735  9t6e54  9736  9t7e63  9737  9t8e72  9738  9t9e81  9739  4bc3eq4  11036  n2dvdsm1  12476  bitsfzo  12518  6gcd4e2  12568  gcdi  12995  2exp8  13010  2exp16  13012  eulerid  15529  cosq23lt0  15560  binom4  15706  lgsdir2lem1  15760  m1lgs  15817  2lgsoddprmlem3d  15842  ex-exp  16340  ex-bc  16342  ex-gcd  16344