Theorem addcomli 8435

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

Syntax hints:   = wceq 1398   ∈ wcel 2205  (class class class)co 6058  ℂcc 8141   + caddc 8146

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216  ax-addcom 8243

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

This theorem is referenced by:  negsubdi2i  8576  1p2e3  9392  peano2z  9633  4t4e16  9828  6t3e18  9834  6t5e30  9836  7t3e21  9839  7t4e28  9840  7t6e42  9842  7t7e49  9843  8t3e24  9845  8t4e32  9846  8t5e40  9847  8t8e64  9850  9t3e27  9852  9t4e36  9853  9t5e45  9854  9t6e54  9855  9t7e63  9856  9t8e72  9857  9t9e81  9858  4bc3eq4  11164  n2dvdsm1  12627  bitsfzo  12669  6gcd4e2  12719  gcdi  13146  2exp8  13161  2exp16  13163  eulerid  15796  cosq23lt0  15827  binom4  15973  lgsdir2lem1  16030  m1lgs  16087  2lgsoddprmlem3d  16112  ex-exp  16624  ex-bc  16626  ex-gcd  16628