Theorem addcomli 8104

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

Syntax hints:   = wceq 1353   ∈ wcel 2148  (class class class)co 5877  ℂcc 7811   + caddc 7816

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159  ax-addcom 7913

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

This theorem is referenced by:  negsubdi2i  8245  1p2e3  9055  peano2z  9291  4t4e16  9484  6t3e18  9490  6t5e30  9492  7t3e21  9495  7t4e28  9496  7t6e42  9498  7t7e49  9499  8t3e24  9501  8t4e32  9502  8t5e40  9503  8t8e64  9506  9t3e27  9508  9t4e36  9509  9t5e45  9510  9t6e54  9511  9t7e63  9512  9t8e72  9513  9t9e81  9514  4bc3eq4  10755  n2dvdsm1  11920  6gcd4e2  11998  eulerid  14262  cosq23lt0  14293  binom4  14436  lgsdir2lem1  14468  m1lgs  14491  2lgsoddprmlem3d  14497  ex-exp  14518  ex-bc  14520  ex-gcd  14522