Theorem addcomli 11386

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

Syntax hints:   = wceq 1561   ∈ wcel 2143  (class class class)co 7396  ℂcc 11082   + caddc 11087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pow 5323  ax-pr 5391  ax-un 7718  ax-resscn 11141  ax-1cn 11142  ax-icn 11143  ax-addcl 11144  ax-addrcl 11145  ax-mulcl 11146  ax-mulrcl 11147  ax-mulcom 11148  ax-addass 11149  ax-mulass 11150  ax-distr 11151  ax-i2m1 11152  ax-1ne0 11153  ax-1rid 11154  ax-rnegex 11155  ax-rrecex 11156  ax-cnre 11157  ax-pre-lttri 11158  ax-pre-lttrn 11159  ax-pre-ltadd 11160

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-opab 5164  df-mpt 5183  df-id 5543  df-po 5556  df-so 5557  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-ov 7399  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11229  df-mnf 11230  df-ltxr 11232

This theorem is referenced by:  mvlladdi  11460  negsubdi2i  11528  1p2e3ALT  12371  4t4e16  12802  6t3e18  12808  6t5e30  12810  7t3e21  12813  7t4e28  12814  7t6e42  12816  7t7e49  12817  8t3e24  12819  8t4e32  12820  8t5e40  12821  8t8e64  12824  9t3e27  12826  9t4e36  12827  9t5e45  12828  9t6e54  12829  9t7e63  12830  9t8e72  12831  9t9e81  12832  n2dvdsm1  16413  bitsfzo  16479  gcdaddmlem  16568  6gcd4e2  16582  gcdi  17119  2exp8  17134  2exp16  17136  37prm  17167  43prm  17168  83prm  17169  139prm  17170  163prm  17171  317prm  17172  631prm  17173  1259lem1  17177  1259lem2  17178  1259lem3  17179  1259lem4  17180  1259lem5  17181  1259prm  17182  2503lem1  17183  2503lem2  17184  2503lem3  17185  2503prm  17186  4001lem1  17187  4001lem2  17188  4001lem4  17190  4001prm  17191  iaa  26396  dvradcnv  26491  eulerid  26546  binom4  26922  log2ublem3  27020  log2ub  27021  lgsdir2lem1  27396  m1lgs  27459  2lgsoddprmlem3d  27484  addsqnreup  27514  ex-exp  30659  ex-bc  30661  ex-gcd  30666  ex-ind-dvds  30670  9p10ne21  30679  vcm  30786  fib5  34704  fib6  34705  hgt750lem  34947  hgt750lem2  34948  60gcd7e1  42627  3exp7  42675  3lexlogpow5ineq1  42676  3lexlogpow5ineq5  42682  aks4d1p1p4  42693  aks4d1p1p5  42697  aks4d1p1  42698  decpmulnc  42901  sqdeccom12  42903  sq3deccom12  42904  235t711  42919  ex-decpmul  42920  sum9cubes  43259  resqrtvalex  44226  imsqrtvalex  44227  inductionexd  44736  lhe4.4ex1a  44896  dirkertrigeqlem1  46663  sqwvfoura  46793  sqwvfourb  46794  fourierswlem  46795  fouriersw  46796  sin5tlem1  47458  fmtno5lem4  48156  257prm  48161  fmtno4nprmfac193  48174  fmtno5faclem3  48181  fmtno5fac  48182  139prmALT  48196  127prm  48199  11t31e341  48345  gbpart8  48381  ackval3  49296  ackval2012  49304  ackval3012  49305