Theorem addcomli 11330

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  (class class class)co 7361  ℂcc 11029   + caddc 11034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7683  ax-resscn 11088  ax-1cn 11089  ax-icn 11090  ax-addcl 11091  ax-addrcl 11092  ax-mulcl 11093  ax-mulrcl 11094  ax-mulcom 11095  ax-addass 11096  ax-mulass 11097  ax-distr 11098  ax-i2m1 11099  ax-1ne0 11100  ax-1rid 11101  ax-rnegex 11102  ax-rrecex 11103  ax-cnre 11104  ax-pre-lttri 11105  ax-pre-lttrn 11106  ax-pre-ltadd 11107

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7364  df-er 8638  df-en 8889  df-dom 8890  df-sdom 8891  df-pnf 11173  df-mnf 11174  df-ltxr 11176

This theorem is referenced by:  mvlladdi  11404  negsubdi2i  11472  1p2e3ALT  12289  4t4e16  12711  6t3e18  12717  6t5e30  12719  7t3e21  12722  7t4e28  12723  7t6e42  12725  7t7e49  12726  8t3e24  12728  8t4e32  12729  8t5e40  12730  8t8e64  12733  9t3e27  12735  9t4e36  12736  9t5e45  12737  9t6e54  12738  9t7e63  12739  9t8e72  12740  9t9e81  12741  n2dvdsm1  16301  bitsfzo  16367  gcdaddmlem  16456  6gcd4e2  16470  gcdi  17006  2exp8  17021  2exp16  17023  37prm  17053  43prm  17054  83prm  17055  139prm  17056  163prm  17057  317prm  17058  631prm  17059  1259lem1  17063  1259lem2  17064  1259lem3  17065  1259lem4  17066  1259lem5  17067  1259prm  17068  2503lem1  17069  2503lem2  17070  2503lem3  17071  2503prm  17072  4001lem1  17073  4001lem2  17074  4001lem4  17076  4001prm  17077  iaa  26294  dvradcnv  26391  eulerid  26444  binom4  26821  log2ublem3  26919  log2ub  26920  lgsdir2lem1  27297  m1lgs  27360  2lgsoddprmlem3d  27385  addsqnreup  27415  ex-exp  30530  ex-bc  30532  ex-gcd  30537  ex-ind-dvds  30541  9p10ne21  30550  vcm  30656  fib5  34575  fib6  34576  hgt750lem  34821  hgt750lem2  34822  60gcd7e1  42338  3exp7  42386  3lexlogpow5ineq1  42387  3lexlogpow5ineq5  42393  aks4d1p1p4  42404  aks4d1p1p5  42408  aks4d1p1  42409  decpmulnc  42620  sqdeccom12  42622  sq3deccom12  42623  235t711  42638  ex-decpmul  42639  sum9cubes  42993  resqrtvalex  43964  imsqrtvalex  43965  inductionexd  44474  lhe4.4ex1a  44648  dirkertrigeqlem1  46419  sqwvfoura  46549  sqwvfourb  46550  fourierswlem  46551  fouriersw  46552  fmtno5lem4  47879  257prm  47884  fmtno4nprmfac193  47897  fmtno5faclem3  47904  fmtno5fac  47905  139prmALT  47919  127prm  47922  11t31e341  48055  gbpart8  48091  ackval3  49006  ackval2012  49014  ackval3012  49015