Theorem addcomd 11483

Description: Addition is commutative. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) (Revised by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
muld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcomd.2	⊢ (𝜑 → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
addcomd	⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Proof of Theorem addcomd

Step	Hyp	Ref	Expression
1		1cnd 11273	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11299	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11304	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11299	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11452	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 18	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11452	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 18	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11452	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 18	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7426	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2804	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11299	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11302	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11302	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2805	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11299	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11299	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11466	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1398	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 235	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11302	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11302	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2803	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11299	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11465	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1398	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 235	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  (class class class)co 7408  ℂcc 11169  1c1 11172   + caddc 11174   · cmul 11176

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7734  ax-resscn 11228  ax-1cn 11229  ax-icn 11230  ax-addcl 11231  ax-addrcl 11232  ax-mulcl 11233  ax-mulrcl 11234  ax-mulcom 11235  ax-addass 11236  ax-mulass 11237  ax-distr 11238  ax-i2m1 11239  ax-1ne0 11240  ax-1rid 11241  ax-rnegex 11242  ax-rrecex 11243  ax-cnre 11244  ax-pre-lttri 11245  ax-pre-lttrn 11246  ax-pre-ltadd 11247

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  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-dif 3901  df-un 3903  df-in 3905  df-ss 3915  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 5542  df-po 5555  df-so 5556  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-ov 7411  df-er 8695  df-en 8952  df-dom 8953  df-sdom 8954  df-pnf 11316  df-mnf 11317  df-ltxr 11319

This theorem is used by:  muladd11r  11494  comraddd  11495  subadd2  11532  pncan  11534  npcan  11537  subcan  11584  mvlladdd  11696  subaddeqd  11700  addrsub  11702  mulsubaddmulsub  11749  ltadd1  11752  leadd2  11754  ltsubadd2  11756  lesubadd2  11758  lesub3d  11903  supadd  12254  ltaddrp2d  13167  lincmb01cmp  13595  iccf1o  13596  elfzoext  13825  modaddabs  14019  muladdmodid  14021  negmod  14027  modadd2mod  14032  modadd12d  14038  modaddmulmod  14049  addmodlteq  14057  expaddz  14217  bcn2m1  14435  bcn2p1  14436  lenrevpfxcctswrd  14828  spllen  14870  splfv2a  14872  relexpaddnn  15171  relexpaddg  15173  rtrclreclem3  15180  remullem  15262  sqreulem  15494  bhmafibid2  15603  climaddc2  15770  iseraltlem2  15817  fsumsplit1  15878  telfsumo  15936  fsumparts  15940  bcxmas  15971  bpoly4  16192  sinadd  16299  sincossq  16311  cos2t  16313  absefi  16331  dvdsaddre2b  16444  pwp1fsum  16528  sadadd2lem2  16587  bitsres  16610  bezoutlem2  16677  bezoutlem4  16679  pythagtrip  16973  pcadd2  17029  vdwapun  17113  vdwlem5  17124  vdwlem6  17125  vdwlem8  17127  gsumsgrpccat  18997  mulgnndir  19274  mulgdirlem  19276  cyccom  19379  efgcpbllemb  19930  ablfacrp  20243  omndmul2  20308  cncrng  21660  rzgrp  21890  icccvx  25232  cnlmod  25422  cphipval  25525  pjthlem1  25719  cmmbl  25816  voliunlem1  25832  dvle  26288  dvcvx  26301  dvfsumlem2  26308  dvfsumlem4  26310  dvfsum2  26315  ply1divex  26416  plymullem1  26494  coeeulem  26504  aaliou3lem6  26638  dvtaylp  26660  ulmcn  26689  abelthlem7  26728  pilem3  26743  lawcos  27107  affineequiv  27114  affineequiv3  27116  heron  27129  dcubic1lem  27134  dcubic2  27135  dcubic  27137  mcubic  27138  quart1lem  27146  quart1  27147  asinlem2  27160  asinsin  27183  cosasin  27195  atanlogaddlem  27204  atanlogadd  27205  cvxcl  27275  lgamgulmlem2  27320  lgamcvg2  27345  lgam1  27354  bposlem9  27582  lgseisenlem1  27665  2sqlem3  27710  2sqblem  27721  2sqmod  27726  addsqn2reu  27731  2sqreulem1  27736  2sqreunnlem1  27739  dchrisumlem2  27780  selberg  27838  selberg2  27841  selberg4  27851  pntrlog2bndlem1  27867  pntlemb  27887  pntlemf  27895  padicabv  27920  colinearalglem2  29418  axsegconlem9  29436  axeuclidlem  29473  revwlk  30200  eupth2lem3lem3  30764  numclwwlk3lem1  30916  smcnlem  31232  ipval2  31242  hhph  31713  pjhthlem1  31926  golem1  32806  stcltrlem1  32811  pythagreim  33270  quad3d  33274  cycpmco2lem3  33622  cycpmco2lem4  33623  cycpmco2lem5  33624  cycpmco2lem6  33625  cycpmco2  33627  archirngz  33683  archiabllem1a  33685  archiabllem1  33687  archiabllem2c  33689  constrrtcc  34300  cos9thpiminplylem1  34347  cos9thpiminplylem2  34348  cos9thpiminplylem3  34349  cos9thpinconstrlem1  34354  ballotlemsdom  35078  fsum2dsub  35170  resconn  35932  iprodgam  36428  faclimlem1  36429  faclimlem3  36431  faclim  36432  iprodfac  36433  fwddifnp1  36852  dnibndlem7  37272  dnibndlem8  37273  knoppndvlem14  37313  bj-bary1  38153  dvtan  38508  itgaddnclem2  38517  itgmulc2nc  38526  ftc1anclem8  38538  dvasin  38542  areacirclem1  38546  lcmineqlem19  43017  aks4d1p1p2  43040  posbezout  43070  sticksstones7  43122  sticksstones12a  43127  sticksstones12  43128  bcle2d  43149  aks6d1c7lem1  43150  quadfac  43175  dffltz  43584  fltbccoprm  43591  flt4lem3  43598  flt4lem5c  43604  flt4lem5d  43605  flt4lem5e  43606  flt4lem7  43609  nna4b4nsq  43610  fltnltalem  43612  3cubeslem2  43634  3cubeslem3l  43635  3cubeslem3r  43636  pellexlem2  43775  pell14qrgt0  43804  rmxyadd  43866  rmxluc  43881  fzmaxdif  43926  acongeq  43928  jm2.19lem2  43935  jm2.26lem3  43946  areaquad  44161  sqrtcval  44585  int-addcomd  45117  int-leftdistd  45123  subadd4b  46220  sub31  46227  coseq0  46796  coskpi2  46798  cosknegpi  46801  fperdvper  46851  dvbdfbdioolem2  46861  dvnmul  46875  dvmptfprodlem  46876  itgsincmulx  46906  itgsbtaddcnst  46914  stoweidlem11  46943  stirlinglem5  47010  stirlinglem7  47012  dirkertrigeqlem1  47030  dirkertrigeqlem2  47031  dirkertrigeqlem3  47032  dirkertrigeq  47033  dirkercncflem2  47036  fourierdlem4  47043  fourierdlem26  47065  fourierdlem40  47079  fourierdlem42  47081  fourierdlem47  47085  fourierdlem63  47101  fourierdlem64  47102  fourierdlem65  47103  fourierdlem74  47112  fourierdlem75  47113  fourierdlem78  47116  fourierdlem79  47117  fourierdlem84  47122  fourierdlem93  47131  fourierdlem103  47141  fourierdlem111  47149  fourierswlem  47162  fouriersw  47163  etransclem32  47198  etransclem46  47212  sge0gtfsumgt  47375  hoidmv1lelem2  47524  hoidmvlelem2  47528  hspmbllem1  47558  smfmullem1  47723  sigarperm  47792  sin5tlem1  47841  sin5tlem5  47845  cjnpoly  47861  2elfz2melfz  48310  m1modmmod  48356  mod2addne  48362  fargshiftfo  48446  ichexmpl2  48474  fmtnorec3  48555  2zrngacmnd  49267  2zrngagrp  49268  ply1mulgsumlem1  49420  ackval1  49715  ackval2  49716  resum2sqorgt0  49743  eenglngeehlnmlem2  49772  rrx2linest2  49778  line2xlem  49787  itsclc0yqsollem1  49796  itsclc0yqsol  49798  itscnhlc0xyqsol  49799  itsclc0xyqsolr  49803  itsclinecirc0b  49808  itsclquadb  49810  2itscplem1  49812  2itscp  49815  onetansqsecsq  50776  crossp3d  50889