Theorem addcomli 8224

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

Syntax hints:   = wceq 1373   ∈ wcel 2177  (class class class)co 5951  ℂcc 7930   + caddc 7935

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188  ax-addcom 8032

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

This theorem is referenced by:  negsubdi2i  8365  1p2e3  9178  peano2z  9415  4t4e16  9609  6t3e18  9615  6t5e30  9617  7t3e21  9620  7t4e28  9621  7t6e42  9623  7t7e49  9624  8t3e24  9626  8t4e32  9627  8t5e40  9628  8t8e64  9631  9t3e27  9633  9t4e36  9634  9t5e45  9635  9t6e54  9636  9t7e63  9637  9t8e72  9638  9t9e81  9639  4bc3eq4  10925  n2dvdsm1  12268  bitsfzo  12310  6gcd4e2  12360  gcdi  12787  2exp8  12802  2exp16  12804  eulerid  15318  cosq23lt0  15349  binom4  15495  lgsdir2lem1  15549  m1lgs  15606  2lgsoddprmlem3d  15631  ex-exp  15737  ex-bc  15739  ex-gcd  15741