Theorem addcomli 11502

Description: Addition is commutative. (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 11501	. 2 ⊢ (𝐵 + 𝐴) = (𝐴 + 𝐵)
4		addcomli.2	. 2 ⊢ (𝐴 + 𝐵) = 𝐶
5	3, 4	eqtri 2783	1 ⊢ (𝐵 + 𝐴) = 𝐶

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11198   + caddc 11203

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-ltxr 11348

This theorem is used by:  mvlladdi  11576  negsubdi2i  11644  1p2e3ALT  12486  4t4e16  12918  6t3e18  12924  6t5e30  12926  7t3e21  12929  7t4e28  12930  7t6e42  12932  7t7e49  12933  8t3e24  12935  8t4e32  12936  8t5e40  12937  8t8e64  12940  9t3e27  12942  9t4e36  12943  9t5e45  12944  9t6e54  12945  9t7e63  12946  9t8e72  12947  9t9e81  12948  n2dvdsm1  16539  bitsfzo  16605  gcdaddmlem  16696  6gcd4e2  16711  gcdi  17251  2exp8  17266  2exp16  17268  37prm  17299  43prm  17300  83prm  17301  139prm  17302  163prm  17303  317prm  17304  631prm  17305  1259lem1  17309  1259lem2  17310  1259lem3  17311  1259lem4  17312  1259lem5  17313  1259prm  17314  2503lem1  17315  2503lem2  17316  2503lem3  17317  2503prm  17318  4001lem1  17319  4001lem2  17320  4001lem4  17322  4001prm  17323  iaaOLD  26652  dvradcnv  26748  eulerid  26803  binom4  27178  log2ublem3  27276  log2ub  27277  lgsdir2lem1  27652  m1lgs  27715  2lgsoddprmlem3d  27740  addsqnreup  27770  ex-exp  31051  ex-bc  31053  ex-gcd  31058  ex-ind-dvds  31062  9p10ne21  31071  vcm  31178  fib5  35079  fib6  35080  hgt750lem  35322  hgt750lem2  35323  60gcd7e1  43098  3exp7  43146  3lexlogpow5ineq1  43147  3lexlogpow5ineq5  43153  aks4d1p1p4  43164  aks4d1p1p5  43168  aks4d1p1  43169  decpmulnc  43387  sqdeccom12  43389  sq3deccom12  43390  235t711  43405  ex-decpmul  43406  sum9cubes  43726  resqrtvalex  44688  imsqrtvalex  44689  inductionexd  45198  lhe4.4ex1a  45356  dirkertrigeqlem1  47151  sqwvfoura  47281  sqwvfourb  47282  fourierswlem  47283  fouriersw  47284  sin5tlem1  47962  fmtno5lem4  48684  257prm  48689  fmtno4nprmfac193  48702  fmtno5faclem3  48709  fmtno5fac  48710  139prmALT  48724  127prm  48727  11t31e341  48873  gbpart8  48909  ackval3  49838  ackval2012  49846  ackval3012  49847