Theorem addcomli 11329

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11028   + caddc 11033

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 7682  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-mulcom 11094  ax-addass 11095  ax-mulass 11096  ax-distr 11097  ax-i2m1 11098  ax-1ne0 11099  ax-1rid 11100  ax-rnegex 11101  ax-rrecex 11102  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105  ax-pre-ltadd 11106

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 7363  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11172  df-mnf 11173  df-ltxr 11175

This theorem is referenced by:  mvlladdi  11403  negsubdi2i  11471  1p2e3ALT  12288  4t4e16  12710  6t3e18  12716  6t5e30  12718  7t3e21  12721  7t4e28  12722  7t6e42  12724  7t7e49  12725  8t3e24  12727  8t4e32  12728  8t5e40  12729  8t8e64  12732  9t3e27  12734  9t4e36  12735  9t5e45  12736  9t6e54  12737  9t7e63  12738  9t8e72  12739  9t9e81  12740  n2dvdsm1  16300  bitsfzo  16366  gcdaddmlem  16455  6gcd4e2  16469  gcdi  17005  2exp8  17020  2exp16  17022  37prm  17052  43prm  17053  83prm  17054  139prm  17055  163prm  17056  317prm  17057  631prm  17058  1259lem1  17062  1259lem2  17063  1259lem3  17064  1259lem4  17065  1259lem5  17066  1259prm  17067  2503lem1  17068  2503lem2  17069  2503lem3  17070  2503prm  17071  4001lem1  17072  4001lem2  17073  4001lem4  17075  4001prm  17076  iaa  26293  dvradcnv  26390  eulerid  26443  binom4  26820  log2ublem3  26918  log2ub  26919  lgsdir2lem1  27296  m1lgs  27359  2lgsoddprmlem3d  27384  addsqnreup  27414  ex-exp  30508  ex-bc  30510  ex-gcd  30515  ex-ind-dvds  30519  9p10ne21  30528  vcm  30634  fib5  34543  fib6  34544  hgt750lem  34789  hgt750lem2  34790  60gcd7e1  42296  3exp7  42344  3lexlogpow5ineq1  42345  3lexlogpow5ineq5  42351  aks4d1p1p4  42362  aks4d1p1p5  42366  aks4d1p1  42367  decpmulnc  42578  sqdeccom12  42580  sq3deccom12  42581  235t711  42596  ex-decpmul  42597  sum9cubes  42951  resqrtvalex  43922  imsqrtvalex  43923  inductionexd  44432  lhe4.4ex1a  44606  dirkertrigeqlem1  46378  sqwvfoura  46508  sqwvfourb  46509  fourierswlem  46510  fouriersw  46511  fmtno5lem4  47838  257prm  47843  fmtno4nprmfac193  47856  fmtno5faclem3  47863  fmtno5fac  47864  139prmALT  47878  127prm  47881  11t31e341  48014  gbpart8  48050  ackval3  48965  ackval2012  48973  ackval3012  48974