Theorem addcomli 8423

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

Syntax hints:   = wceq 1398   ∈ wcel 2205  (class class class)co 6052  ℂcc 8130   + caddc 8135

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 8232

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

This theorem is referenced by:  negsubdi2i  8564  1p2e3  9377  peano2z  9618  4t4e16  9813  6t3e18  9819  6t5e30  9821  7t3e21  9824  7t4e28  9825  7t6e42  9827  7t7e49  9828  8t3e24  9830  8t4e32  9831  8t5e40  9832  8t8e64  9835  9t3e27  9837  9t4e36  9838  9t5e45  9839  9t6e54  9840  9t7e63  9841  9t8e72  9842  9t9e81  9843  4bc3eq4  11144  n2dvdsm1  12607  bitsfzo  12649  6gcd4e2  12699  gcdi  13126  2exp8  13141  2exp16  13143  eulerid  15716  cosq23lt0  15747  binom4  15893  lgsdir2lem1  15950  m1lgs  16007  2lgsoddprmlem3d  16032  ex-exp  16544  ex-bc  16546  ex-gcd  16548