Theorem addcomli 11326

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  (class class class)co 7358  ℂcc 11025   + caddc 11030

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 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-addrcl 11088  ax-mulcl 11089  ax-mulrcl 11090  ax-mulcom 11091  ax-addass 11092  ax-mulass 11093  ax-distr 11094  ax-i2m1 11095  ax-1ne0 11096  ax-1rid 11097  ax-rnegex 11098  ax-rrecex 11099  ax-cnre 11100  ax-pre-lttri 11101  ax-pre-lttrn 11102  ax-pre-ltadd 11103

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 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-po 5530  df-so 5531  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7361  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11169  df-mnf 11170  df-ltxr 11172

This theorem is referenced by:  mvlladdi  11400  negsubdi2i  11468  1p2e3ALT  12285  4t4e16  12707  6t3e18  12713  6t5e30  12715  7t3e21  12718  7t4e28  12719  7t6e42  12721  7t7e49  12722  8t3e24  12724  8t4e32  12725  8t5e40  12726  8t8e64  12729  9t3e27  12731  9t4e36  12732  9t5e45  12733  9t6e54  12734  9t7e63  12735  9t8e72  12736  9t9e81  12737  n2dvdsm1  16297  bitsfzo  16363  gcdaddmlem  16452  6gcd4e2  16466  gcdi  17002  2exp8  17017  2exp16  17019  37prm  17049  43prm  17050  83prm  17051  139prm  17052  163prm  17053  317prm  17054  631prm  17055  1259lem1  17059  1259lem2  17060  1259lem3  17061  1259lem4  17062  1259lem5  17063  1259prm  17064  2503lem1  17065  2503lem2  17066  2503lem3  17067  2503prm  17068  4001lem1  17069  4001lem2  17070  4001lem4  17072  4001prm  17073  iaa  26273  dvradcnv  26370  eulerid  26423  binom4  26800  log2ublem3  26898  log2ub  26899  lgsdir2lem1  27276  m1lgs  27339  2lgsoddprmlem3d  27364  addsqnreup  27394  ex-exp  30509  ex-bc  30511  ex-gcd  30516  ex-ind-dvds  30520  9p10ne21  30529  vcm  30636  fib5  34555  fib6  34556  hgt750lem  34801  hgt750lem2  34802  60gcd7e1  42436  3exp7  42484  3lexlogpow5ineq1  42485  3lexlogpow5ineq5  42491  aks4d1p1p4  42502  aks4d1p1p5  42506  aks4d1p1  42507  decpmulnc  42718  sqdeccom12  42720  sq3deccom12  42721  235t711  42736  ex-decpmul  42737  sum9cubes  43104  resqrtvalex  44075  imsqrtvalex  44076  inductionexd  44585  lhe4.4ex1a  44759  dirkertrigeqlem1  46530  sqwvfoura  46660  sqwvfourb  46661  fourierswlem  46662  fouriersw  46663  fmtno5lem4  47990  257prm  47995  fmtno4nprmfac193  48008  fmtno5faclem3  48015  fmtno5fac  48016  139prmALT  48030  127prm  48033  11t31e341  48166  gbpart8  48202  ackval3  49117  ackval2012  49125  ackval3012  49126