Theorem addcomli 11311

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

Syntax hints:   = wceq 1541   ∈ wcel 2111  (class class class)co 7352  ℂcc 11010   + caddc 11015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-resscn 11069  ax-1cn 11070  ax-icn 11071  ax-addcl 11072  ax-addrcl 11073  ax-mulcl 11074  ax-mulrcl 11075  ax-mulcom 11076  ax-addass 11077  ax-mulass 11078  ax-distr 11079  ax-i2m1 11080  ax-1ne0 11081  ax-1rid 11082  ax-rnegex 11083  ax-rrecex 11084  ax-cnre 11085  ax-pre-lttri 11086  ax-pre-lttrn 11087  ax-pre-ltadd 11088

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-ov 7355  df-er 8628  df-en 8876  df-dom 8877  df-sdom 8878  df-pnf 11154  df-mnf 11155  df-ltxr 11157

This theorem is referenced by:  mvlladdi  11385  negsubdi2i  11453  1p2e3ALT  12270  4t4e16  12693  6t3e18  12699  6t5e30  12701  7t3e21  12704  7t4e28  12705  7t6e42  12707  7t7e49  12708  8t3e24  12710  8t4e32  12711  8t5e40  12712  8t8e64  12715  9t3e27  12717  9t4e36  12718  9t5e45  12719  9t6e54  12720  9t7e63  12721  9t8e72  12722  9t9e81  12723  n2dvdsm1  16286  bitsfzo  16352  gcdaddmlem  16441  6gcd4e2  16455  gcdi  16991  2exp8  17006  2exp16  17008  37prm  17038  43prm  17039  83prm  17040  139prm  17041  163prm  17042  317prm  17043  631prm  17044  1259lem1  17048  1259lem2  17049  1259lem3  17050  1259lem4  17051  1259lem5  17052  1259prm  17053  2503lem1  17054  2503lem2  17055  2503lem3  17056  2503prm  17057  4001lem1  17058  4001lem2  17059  4001lem4  17061  4001prm  17062  iaa  26266  dvradcnv  26363  eulerid  26416  binom4  26793  log2ublem3  26891  log2ub  26892  lgsdir2lem1  27269  m1lgs  27332  2lgsoddprmlem3d  27357  addsqnreup  27387  ex-exp  30437  ex-bc  30439  ex-gcd  30444  ex-ind-dvds  30448  9p10ne21  30457  vcm  30563  fib5  34425  fib6  34426  hgt750lem  34671  hgt750lem2  34672  60gcd7e1  42104  3exp7  42152  3lexlogpow5ineq1  42153  3lexlogpow5ineq5  42159  aks4d1p1p4  42170  aks4d1p1p5  42174  aks4d1p1  42175  decpmulnc  42386  sqdeccom12  42388  sq3deccom12  42389  235t711  42404  ex-decpmul  42405  sum9cubes  42771  resqrtvalex  43743  imsqrtvalex  43744  inductionexd  44253  lhe4.4ex1a  44427  dirkertrigeqlem1  46201  sqwvfoura  46331  sqwvfourb  46332  fourierswlem  46333  fouriersw  46334  fmtno5lem4  47661  257prm  47666  fmtno4nprmfac193  47679  fmtno5faclem3  47686  fmtno5fac  47687  139prmALT  47701  127prm  47704  11t31e341  47837  gbpart8  47873  ackval3  48789  ackval2012  48797  ackval3012  48798