Theorem addcomli 11372

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7389  ℂcc 11072   + caddc 11077

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5253  ax-nul 5263  ax-pow 5322  ax-pr 5389  ax-un 7713  ax-resscn 11131  ax-1cn 11132  ax-icn 11133  ax-addcl 11134  ax-addrcl 11135  ax-mulcl 11136  ax-mulrcl 11137  ax-mulcom 11138  ax-addass 11139  ax-mulass 11140  ax-distr 11141  ax-i2m1 11142  ax-1ne0 11143  ax-1rid 11144  ax-rnegex 11145  ax-rrecex 11146  ax-cnre 11147  ax-pre-lttri 11148  ax-pre-lttrn 11149  ax-pre-ltadd 11150

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3756  df-csb 3865  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-nul 4299  df-if 4491  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-opab 5172  df-mpt 5191  df-id 5535  df-po 5548  df-so 5549  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-iota 6466  df-fun 6515  df-fn 6516  df-f 6517  df-f1 6518  df-fo 6519  df-f1o 6520  df-fv 6521  df-ov 7392  df-er 8673  df-en 8921  df-dom 8922  df-sdom 8923  df-pnf 11216  df-mnf 11217  df-ltxr 11219

This theorem is referenced by:  mvlladdi  11446  negsubdi2i  11514  1p2e3ALT  12331  4t4e16  12754  6t3e18  12760  6t5e30  12762  7t3e21  12765  7t4e28  12766  7t6e42  12768  7t7e49  12769  8t3e24  12771  8t4e32  12772  8t5e40  12773  8t8e64  12776  9t3e27  12778  9t4e36  12779  9t5e45  12780  9t6e54  12781  9t7e63  12782  9t8e72  12783  9t9e81  12784  n2dvdsm1  16345  bitsfzo  16411  gcdaddmlem  16500  6gcd4e2  16514  gcdi  17050  2exp8  17065  2exp16  17067  37prm  17097  43prm  17098  83prm  17099  139prm  17100  163prm  17101  317prm  17102  631prm  17103  1259lem1  17107  1259lem2  17108  1259lem3  17109  1259lem4  17110  1259lem5  17111  1259prm  17112  2503lem1  17113  2503lem2  17114  2503lem3  17115  2503prm  17116  4001lem1  17117  4001lem2  17118  4001lem4  17120  4001prm  17121  iaa  26239  dvradcnv  26336  eulerid  26389  binom4  26766  log2ublem3  26864  log2ub  26865  lgsdir2lem1  27242  m1lgs  27305  2lgsoddprmlem3d  27330  addsqnreup  27360  ex-exp  30385  ex-bc  30387  ex-gcd  30392  ex-ind-dvds  30396  9p10ne21  30405  vcm  30511  fib5  34402  fib6  34403  hgt750lem  34648  hgt750lem2  34649  60gcd7e1  41988  3exp7  42036  3lexlogpow5ineq1  42037  3lexlogpow5ineq5  42043  aks4d1p1p4  42054  aks4d1p1p5  42058  aks4d1p1  42059  decpmulnc  42270  sqdeccom12  42272  sq3deccom12  42273  235t711  42288  ex-decpmul  42289  sum9cubes  42653  resqrtvalex  43627  imsqrtvalex  43628  inductionexd  44137  lhe4.4ex1a  44311  dirkertrigeqlem1  46089  sqwvfoura  46219  sqwvfourb  46220  fourierswlem  46221  fouriersw  46222  fmtno5lem4  47547  257prm  47552  fmtno4nprmfac193  47565  fmtno5faclem3  47572  fmtno5fac  47573  139prmALT  47587  127prm  47590  11t31e341  47723  gbpart8  47759  ackval3  48662  ackval2012  48670  ackval3012  48671