Theorem addcomli 8479

Description: Addition is commutative. (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 8478	. 2 ⊢ (𝐵 + 𝐴) = (𝐴 + 𝐵)
4		addcomli.2	. 2 ⊢ (𝐴 + 𝐵) = 𝐶
5	3, 4	eqtri 2259	1 ⊢ (𝐵 + 𝐴) = 𝐶

This proof depends on syntax axioms:   = wceq 1402   ∈ wcel 2209  (class class class)co 6088  ℂcc 8184   + caddc 8189

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220  ax-addcom 8286

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  negsubdi2i  8620  1p2e3  9449  peano2z  9692  4t4e16  9892  6t3e18  9898  6t5e30  9900  7t3e21  9903  7t4e28  9904  7t6e42  9906  7t7e49  9907  8t3e24  9909  8t4e32  9910  8t5e40  9911  8t8e64  9914  9t3e27  9916  9t4e36  9917  9t5e45  9918  9t6e54  9919  9t7e63  9920  9t8e72  9921  9t9e81  9922  4bc3eq4  11235  n2dvdsm1  12706  bitsfzo  12748  6gcd4e2  12798  gcdi  13230  2exp8  13245  2exp16  13247  37prm  13265  43prm  13266  83prm  13267  139prm  13268  163prm  13269  317prm  13270  631prm  13271  1259lem1  13272  1259lem2  13273  1259lem3  13274  1259lem4  13275  1259lem5  13276  1259prm  13277  eulerid  16041  cosq23lt0  16072  binom4  16231  log2ublem3  16235  log2ublog2  16236  lgsdir2lem1  16364  m1lgs  16421  2lgsoddprmlem3d  16446  ex-exp  16958  ex-bc  16960  ex-gcd  16962