Theorem addcomli 10679

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

Syntax hints:   = wceq 1522   ∈ wcel 2081  (class class class)co 7016  ℂcc 10381   + caddc 10386

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-resscn 10440  ax-1cn 10441  ax-icn 10442  ax-addcl 10443  ax-addrcl 10444  ax-mulcl 10445  ax-mulrcl 10446  ax-mulcom 10447  ax-addass 10448  ax-mulass 10449  ax-distr 10450  ax-i2m1 10451  ax-1ne0 10452  ax-1rid 10453  ax-rnegex 10454  ax-rrecex 10455  ax-cnre 10456  ax-pre-lttri 10457  ax-pre-lttrn 10458  ax-pre-ltadd 10459

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-mpt 5042  df-id 5348  df-po 5362  df-so 5363  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-ov 7019  df-er 8139  df-en 8358  df-dom 8359  df-sdom 8360  df-pnf 10523  df-mnf 10524  df-ltxr 10526

This theorem is referenced by:  mvlladdi  10752  negsubdi2i  10820  1p2e3ALT  11629  4t4e16  12047  6t3e18  12053  6t5e30  12055  7t3e21  12058  7t4e28  12059  7t6e42  12061  7t7e49  12062  8t3e24  12064  8t4e32  12065  8t5e40  12066  8t8e64  12069  9t3e27  12071  9t4e36  12072  9t5e45  12073  9t6e54  12074  9t7e63  12075  9t8e72  12076  9t9e81  12077  n2dvdsm1  15552  bitsfzo  15617  gcdaddmlem  15705  6gcd4e2  15715  gcdi  16238  2exp8  16252  2exp16  16253  37prm  16283  43prm  16284  83prm  16285  139prm  16286  163prm  16287  317prm  16288  631prm  16289  1259lem1  16293  1259lem2  16294  1259lem3  16295  1259lem4  16296  1259lem5  16297  1259prm  16298  2503lem1  16299  2503lem2  16300  2503lem3  16301  2503prm  16302  4001lem1  16303  4001lem2  16304  4001lem4  16306  4001prm  16307  iaa  24597  dvradcnv  24692  eulerid  24743  binom4  25109  log2ublem3  25208  log2ub  25209  lgsdir2lem1  25583  m1lgs  25646  2lgsoddprmlem3d  25671  addsqnreup  25701  ex-exp  27921  ex-bc  27923  ex-gcd  27928  ex-ind-dvds  27932  9p10ne21  27940  vcm  28044  fib5  31280  fib6  31281  hgt750lem  31539  hgt750lem2  31540  decpmulnc  38695  sqdeccom12  38697  sq3deccom12  38698  235t711  38699  ex-decpmul  38700  inductionexd  39990  lhe4.4ex1a  40199  dirkertrigeqlem1  41925  sqwvfoura  42055  sqwvfourb  42056  fourierswlem  42057  fouriersw  42058  fmtno5lem4  43200  257prm  43205  fmtno4nprmfac193  43218  fmtno5faclem3  43225  fmtno5fac  43226  139prmALT  43241  127prm  43245  11t31e341  43379  gbpart8  43415