Theorem addcomli 8414

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

Syntax hints:   = wceq 1398   ∈ wcel 2203  (class class class)co 6049  ℂcc 8121   + caddc 8126

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 2214  ax-addcom 8223

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

This theorem is referenced by:  negsubdi2i  8555  1p2e3  9368  peano2z  9609  4t4e16  9803  6t3e18  9809  6t5e30  9811  7t3e21  9814  7t4e28  9815  7t6e42  9817  7t7e49  9818  8t3e24  9820  8t4e32  9821  8t5e40  9822  8t8e64  9825  9t3e27  9827  9t4e36  9828  9t5e45  9829  9t6e54  9830  9t7e63  9831  9t8e72  9832  9t9e81  9833  4bc3eq4  11131  n2dvdsm1  12592  bitsfzo  12634  6gcd4e2  12684  gcdi  13111  2exp8  13126  2exp16  13128  eulerid  15654  cosq23lt0  15685  binom4  15831  lgsdir2lem1  15888  m1lgs  15945  2lgsoddprmlem3d  15970  ex-exp  16482  ex-bc  16484  ex-gcd  16486