Theorem addcomli 8299

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

Syntax hints:   = wceq 1395   ∈ wcel 2200  (class class class)co 6007  ℂcc 8005   + caddc 8010

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211  ax-addcom 8107

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

This theorem is referenced by:  negsubdi2i  8440  1p2e3  9253  peano2z  9490  4t4e16  9684  6t3e18  9690  6t5e30  9692  7t3e21  9695  7t4e28  9696  7t6e42  9698  7t7e49  9699  8t3e24  9701  8t4e32  9702  8t5e40  9703  8t8e64  9706  9t3e27  9708  9t4e36  9709  9t5e45  9710  9t6e54  9711  9t7e63  9712  9t8e72  9713  9t9e81  9714  4bc3eq4  11003  n2dvdsm1  12432  bitsfzo  12474  6gcd4e2  12524  gcdi  12951  2exp8  12966  2exp16  12968  eulerid  15484  cosq23lt0  15515  binom4  15661  lgsdir2lem1  15715  m1lgs  15772  2lgsoddprmlem3d  15797  ex-exp  16115  ex-bc  16117  ex-gcd  16119