Theorem addcomli 8190

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

Syntax hints:   = wceq 1364   ∈ wcel 2167  (class class class)co 5925  ℂcc 7896   + caddc 7901

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178  ax-addcom 7998

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

This theorem is referenced by:  negsubdi2i  8331  1p2e3  9144  peano2z  9381  4t4e16  9574  6t3e18  9580  6t5e30  9582  7t3e21  9585  7t4e28  9586  7t6e42  9588  7t7e49  9589  8t3e24  9591  8t4e32  9592  8t5e40  9593  8t8e64  9596  9t3e27  9598  9t4e36  9599  9t5e45  9600  9t6e54  9601  9t7e63  9602  9t8e72  9603  9t9e81  9604  4bc3eq4  10884  n2dvdsm1  12097  bitsfzo  12139  6gcd4e2  12189  gcdi  12616  2exp8  12631  2exp16  12633  eulerid  15124  cosq23lt0  15155  binom4  15301  lgsdir2lem1  15355  m1lgs  15412  2lgsoddprmlem3d  15437  ex-exp  15459  ex-bc  15461  ex-gcd  15463