Theorem addcomli 11338

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036   + caddc 11041

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 5232  ax-nul 5242  ax-pow 5308  ax-pr 5376  ax-un 7689  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114

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 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6455  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7370  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-ltxr 11184

This theorem is referenced by:  mvlladdi  11412  negsubdi2i  11480  1p2e3ALT  12320  4t4e16  12743  6t3e18  12749  6t5e30  12751  7t3e21  12754  7t4e28  12755  7t6e42  12757  7t7e49  12758  8t3e24  12760  8t4e32  12761  8t5e40  12762  8t8e64  12765  9t3e27  12767  9t4e36  12768  9t5e45  12769  9t6e54  12770  9t7e63  12771  9t8e72  12772  9t9e81  12773  n2dvdsm1  16338  bitsfzo  16404  gcdaddmlem  16493  6gcd4e2  16507  gcdi  17044  2exp8  17059  2exp16  17061  37prm  17091  43prm  17092  83prm  17093  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem4  17114  4001prm  17115  iaa  26291  dvradcnv  26386  eulerid  26438  binom4  26814  log2ublem3  26912  log2ub  26913  lgsdir2lem1  27288  m1lgs  27351  2lgsoddprmlem3d  27376  addsqnreup  27406  ex-exp  30520  ex-bc  30522  ex-gcd  30527  ex-ind-dvds  30531  9p10ne21  30540  vcm  30647  fib5  34549  fib6  34550  hgt750lem  34795  hgt750lem2  34796  60gcd7e1  42444  3exp7  42492  3lexlogpow5ineq1  42493  3lexlogpow5ineq5  42499  aks4d1p1p4  42510  aks4d1p1p5  42514  aks4d1p1  42515  decpmulnc  42719  sqdeccom12  42721  sq3deccom12  42722  235t711  42737  ex-decpmul  42738  sum9cubes  43105  resqrtvalex  44072  imsqrtvalex  44073  inductionexd  44582  lhe4.4ex1a  44756  dirkertrigeqlem1  46526  sqwvfoura  46656  sqwvfourb  46657  fourierswlem  46658  fouriersw  46659  sin5tlem1  47319  fmtno5lem4  48013  257prm  48018  fmtno4nprmfac193  48031  fmtno5faclem3  48038  fmtno5fac  48039  139prmALT  48053  127prm  48056  11t31e341  48202  gbpart8  48238  ackval3  49153  ackval2012  49161  ackval3012  49162