Theorem addcomd 11418

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 11208	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11234	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11239	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11234	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11387	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 18	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11387	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 18	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11387	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 18	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7430	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2806	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11234	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11237	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11237	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2807	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11234	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11234	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11401	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1397	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 235	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11237	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11237	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2805	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11234	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11400	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1397	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 235	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2142  (class class class)co 7412  ℂcc 11104  1c1 11107   + caddc 11109   · cmul 11111

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5555  df-po 5568  df-so 5569  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7415  df-er 8692  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11251  df-mnf 11252  df-ltxr 11254

This theorem is used by:  muladd11r  11429  comraddd  11430  subadd2  11467  pncan  11469  npcan  11472  subcan  11519  mvlladdd  11631  subaddeqd  11635  addrsub  11637  mulsubaddmulsub  11684  ltadd1  11687  leadd2  11689  ltsubadd2  11691  lesubadd2  11693  lesub3d  11838  supadd  12189  ltaddrp2d  13100  lincmb01cmp  13528  iccf1o  13529  elfzoext  13758  modaddabs  13951  muladdmodid  13953  negmod  13959  modadd2mod  13964  modadd12d  13970  modaddmulmod  13981  addmodlteq  13989  expaddz  14149  bcn2m1  14367  bcn2p1  14368  lenrevpfxcctswrd  14756  spllen  14798  splfv2a  14800  relexpaddnn  15095  relexpaddg  15097  rtrclreclem3  15104  remullem  15186  sqreulem  15418  bhmafibid2  15527  climaddc2  15694  iseraltlem2  15741  fsumsplit1  15803  telfsumo  15861  fsumparts  15865  bcxmas  15896  bpoly4  16119  sinadd  16226  sincossq  16238  cos2t  16240  absefi  16258  dvdsaddre2b  16371  pwp1fsum  16455  sadadd2lem2  16514  bitsres  16537  bezoutlem2  16604  bezoutlem4  16606  pythagtrip  16900  pcadd2  16956  vdwapun  17040  vdwlem5  17051  vdwlem6  17052  vdwlem8  17054  gsumsgrpccat  18905  mulgnndir  19175  mulgdirlem  19177  cyccom  19280  efgcpbllemb  19831  ablfacrp  20144  omndmul2  20209  cncrng  21554  rzgrp  21784  icccvx  25120  cnlmod  25310  cphipval  25413  pjthlem1  25607  cmmbl  25704  voliunlem1  25720  dvle  26177  dvcvx  26190  dvfsumlem2  26197  dvfsumlem4  26199  dvfsum2  26204  ply1divex  26305  plymullem1  26382  coeeulem  26392  aaliou3lem6  26522  dvtaylp  26544  ulmcn  26573  abelthlem7  26612  pilem3  26627  lawcos  26992  affineequiv  26999  affineequiv3  27001  heron  27014  dcubic1lem  27019  dcubic2  27020  dcubic  27022  mcubic  27023  quart1lem  27031  quart1  27032  asinlem2  27045  asinsin  27068  cosasin  27080  atanlogaddlem  27089  atanlogadd  27090  cvxcl  27160  lgamgulmlem2  27205  lgamcvg2  27230  lgam1  27239  bposlem9  27467  lgseisenlem1  27550  2sqlem3  27595  2sqblem  27606  2sqmod  27611  addsqn2reu  27616  2sqreulem1  27621  2sqreunnlem1  27624  dchrisumlem2  27665  selberg  27723  selberg2  27726  selberg4  27736  pntrlog2bndlem1  27752  pntlemb  27772  pntlemf  27780  padicabv  27805  colinearalglem2  29268  axsegconlem9  29286  axeuclidlem  29323  eupth2lem3lem3  30592  numclwwlk3lem1  30744  smcnlem  31060  ipval2  31070  hhph  31541  pjhthlem1  31754  golem1  32634  stcltrlem1  32639  pythagreim  33101  quad3d  33105  cycpmco2lem3  33457  cycpmco2lem4  33458  cycpmco2lem5  33459  cycpmco2lem6  33460  cycpmco2  33462  archirngz  33518  archiabllem1a  33520  archiabllem1  33522  archiabllem2c  33524  constrrtcc  34134  cos9thpiminplylem1  34181  cos9thpiminplylem2  34182  cos9thpiminplylem3  34183  cos9thpinconstrlem1  34188  ballotlemsdom  34911  fsum2dsub  35003  revwlk  35625  resconn  35746  iprodgam  36242  faclimlem1  36243  faclimlem3  36245  faclim  36246  iprodfac  36247  fwddifnp1  36665  dnibndlem7  37101  dnibndlem8  37102  knoppndvlem14  37142  bj-bary1  37984  dvtan  38349  itgaddnclem2  38358  itgmulc2nc  38367  ftc1anclem8  38379  dvasin  38383  areacirclem1  38387  lcmineqlem19  42842  aks4d1p1p2  42865  posbezout  42895  sticksstones7  42947  sticksstones12a  42952  sticksstones12  42953  bcle2d  42974  aks6d1c7lem1  42975  quadfac  43000  dffltz  43394  fltbccoprm  43401  flt4lem3  43408  flt4lem5c  43414  flt4lem5d  43415  flt4lem5e  43416  flt4lem7  43419  nna4b4nsq  43420  fltnltalem  43422  3cubeslem2  43444  3cubeslem3l  43445  3cubeslem3r  43446  pellexlem2  43585  pell14qrgt0  43614  rmxyadd  43676  rmxluc  43691  fzmaxdif  43736  acongeq  43738  jm2.19lem2  43745  jm2.26lem3  43756  areaquad  43971  sqrtcval  44395  int-addcomd  44927  int-leftdistd  44933  subadd4b  46030  sub31  46037  coseq0  46606  coskpi2  46608  cosknegpi  46611  fperdvper  46661  dvbdfbdioolem2  46671  dvnmul  46685  dvmptfprodlem  46686  itgsincmulx  46716  itgsbtaddcnst  46724  stoweidlem11  46753  stirlinglem5  46820  stirlinglem7  46822  dirkertrigeqlem1  46840  dirkertrigeqlem2  46841  dirkertrigeqlem3  46842  dirkertrigeq  46843  dirkercncflem2  46846  fourierdlem4  46853  fourierdlem26  46875  fourierdlem40  46889  fourierdlem42  46891  fourierdlem47  46895  fourierdlem63  46911  fourierdlem64  46912  fourierdlem65  46913  fourierdlem74  46922  fourierdlem75  46923  fourierdlem78  46926  fourierdlem79  46927  fourierdlem84  46932  fourierdlem93  46941  fourierdlem103  46951  fourierdlem111  46959  fourierswlem  46972  fouriersw  46973  etransclem32  47008  etransclem46  47022  sge0gtfsumgt  47185  hoidmv1lelem2  47334  hoidmvlelem2  47338  hspmbllem1  47368  smfmullem1  47533  sigarperm  47602  sin5tlem1  47638  sin5tlem5  47642  cjnpoly  47654  2elfz2melfz  48083  m1modmmod  48129  mod2addne  48135  fargshiftfo  48219  ichexmpl2  48247  fmtnorec3  48328  2zrngacmnd  49041  2zrngagrp  49042  ply1mulgsumlem1  49194  ackval1  49489  ackval2  49490  resum2sqorgt0  49517  eenglngeehlnmlem2  49546  rrx2linest2  49552  line2xlem  49561  itsclc0yqsollem1  49570  itsclc0yqsol  49572  itscnhlc0xyqsol  49573  itsclc0xyqsolr  49577  itsclinecirc0b  49582  itsclquadb  49584  2itscplem1  49586  2itscp  49589  onetansqsecsq  50567  crossp3i  50676