Theorem addcomli 11361

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

Syntax hints:   = wceq 1550   ∈ wcel 2132  (class class class)co 7381  ℂcc 11057   + caddc 11062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pow 5312  ax-pr 5380  ax-un 7703  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-nel 3052  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-sbc 3736  df-csb 3844  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-opab 5153  df-mpt 5172  df-id 5531  df-po 5544  df-so 5545  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649  df-iota 6462  df-fun 6508  df-fn 6509  df-f 6510  df-f1 6511  df-fo 6512  df-f1o 6513  df-fv 6514  df-ov 7384  df-er 8662  df-en 8913  df-dom 8914  df-sdom 8915  df-pnf 11204  df-mnf 11205  df-ltxr 11207

This theorem is referenced by:  mvlladdi  11435  negsubdi2i  11503  1p2e3ALT  12347  4t4e16  12778  6t3e18  12784  6t5e30  12786  7t3e21  12789  7t4e28  12790  7t6e42  12792  7t7e49  12793  8t3e24  12795  8t4e32  12796  8t5e40  12797  8t8e64  12800  9t3e27  12802  9t4e36  12803  9t5e45  12804  9t6e54  12805  9t7e63  12806  9t8e72  12807  9t9e81  12808  n2dvdsm1  16375  bitsfzo  16441  gcdaddmlem  16530  6gcd4e2  16544  gcdi  17081  2exp8  17096  2exp16  17098  37prm  17129  43prm  17130  83prm  17131  139prm  17132  163prm  17133  317prm  17134  631prm  17135  1259lem1  17139  1259lem2  17140  1259lem3  17141  1259lem4  17142  1259lem5  17143  1259prm  17144  2503lem1  17145  2503lem2  17146  2503lem3  17147  2503prm  17148  4001lem1  17149  4001lem2  17150  4001lem4  17152  4001prm  17153  iaa  26355  dvradcnv  26450  eulerid  26505  binom4  26881  log2ublem3  26979  log2ub  26980  lgsdir2lem1  27355  m1lgs  27418  2lgsoddprmlem3d  27443  addsqnreup  27473  ex-exp  30587  ex-bc  30589  ex-gcd  30594  ex-ind-dvds  30598  9p10ne21  30607  vcm  30714  fib5  34646  fib6  34647  hgt750lem  34892  hgt750lem2  34893  60gcd7e1  42560  3exp7  42608  3lexlogpow5ineq1  42609  3lexlogpow5ineq5  42615  aks4d1p1p4  42626  aks4d1p1p5  42630  aks4d1p1  42631  decpmulnc  42834  sqdeccom12  42836  sq3deccom12  42837  235t711  42852  ex-decpmul  42853  sum9cubes  43192  resqrtvalex  44159  imsqrtvalex  44160  inductionexd  44669  lhe4.4ex1a  44843  dirkertrigeqlem1  46610  sqwvfoura  46740  sqwvfourb  46741  fourierswlem  46742  fouriersw  46743  sin5tlem1  47405  fmtno5lem4  48103  257prm  48108  fmtno4nprmfac193  48121  fmtno5faclem3  48128  fmtno5fac  48129  139prmALT  48143  127prm  48146  11t31e341  48292  gbpart8  48328  ackval3  49243  ackval2012  49251  ackval3012  49252