Theorem addcomd 11439

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 11229	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11255	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11260	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11255	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11408	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 18	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11408	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 18	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11408	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 18	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7434	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2806	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11255	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11258	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11258	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2807	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11255	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11255	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11422	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1398	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 235	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11258	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11258	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2805	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11255	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11421	. . 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 7416  ℂcc 11125  1c1 11128   + caddc 11130   · cmul 11132

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 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203

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 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 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7419  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-ltxr 11275

This theorem is used by:  muladd11r  11450  comraddd  11451  subadd2  11488  pncan  11490  npcan  11493  subcan  11540  mvlladdd  11652  subaddeqd  11656  addrsub  11658  mulsubaddmulsub  11705  ltadd1  11708  leadd2  11710  ltsubadd2  11712  lesubadd2  11714  lesub3d  11859  supadd  12210  ltaddrp2d  13122  lincmb01cmp  13550  iccf1o  13551  elfzoext  13780  modaddabs  13974  muladdmodid  13976  negmod  13982  modadd2mod  13987  modadd12d  13993  modaddmulmod  14004  addmodlteq  14012  expaddz  14172  bcn2m1  14390  bcn2p1  14391  lenrevpfxcctswrd  14783  spllen  14825  splfv2a  14827  relexpaddnn  15126  relexpaddg  15128  rtrclreclem3  15135  remullem  15217  sqreulem  15449  bhmafibid2  15558  climaddc2  15725  iseraltlem2  15772  fsumsplit1  15833  telfsumo  15891  fsumparts  15895  bcxmas  15926  bpoly4  16149  sinadd  16256  sincossq  16268  cos2t  16270  absefi  16288  dvdsaddre2b  16401  pwp1fsum  16485  sadadd2lem2  16544  bitsres  16567  bezoutlem2  16634  bezoutlem4  16636  pythagtrip  16930  pcadd2  16986  vdwapun  17070  vdwlem5  17081  vdwlem6  17082  vdwlem8  17084  gsumsgrpccat  18950  mulgnndir  19227  mulgdirlem  19229  cyccom  19332  efgcpbllemb  19883  ablfacrp  20196  omndmul2  20261  cncrng  21607  rzgrp  21837  icccvx  25179  cnlmod  25369  cphipval  25472  pjthlem1  25666  cmmbl  25763  voliunlem1  25779  dvle  26236  dvcvx  26249  dvfsumlem2  26256  dvfsumlem4  26258  dvfsum2  26263  ply1divex  26364  plymullem1  26441  coeeulem  26451  aaliou3lem6  26581  dvtaylp  26603  ulmcn  26632  abelthlem7  26671  pilem3  26686  lawcos  27051  affineequiv  27058  affineequiv3  27060  heron  27073  dcubic1lem  27078  dcubic2  27079  dcubic  27081  mcubic  27082  quart1lem  27090  quart1  27091  asinlem2  27104  asinsin  27127  cosasin  27139  atanlogaddlem  27148  atanlogadd  27149  cvxcl  27219  lgamgulmlem2  27264  lgamcvg2  27289  lgam1  27298  bposlem9  27526  lgseisenlem1  27609  2sqlem3  27654  2sqblem  27665  2sqmod  27670  addsqn2reu  27675  2sqreulem1  27680  2sqreunnlem1  27683  dchrisumlem2  27724  selberg  27782  selberg2  27785  selberg4  27795  pntrlog2bndlem1  27811  pntlemb  27831  pntlemf  27839  padicabv  27864  colinearalglem2  29350  axsegconlem9  29368  axeuclidlem  29405  revwlk  30132  eupth2lem3lem3  30696  numclwwlk3lem1  30848  smcnlem  31164  ipval2  31174  hhph  31645  pjhthlem1  31858  golem1  32738  stcltrlem1  32743  pythagreim  33203  quad3d  33207  cycpmco2lem3  33555  cycpmco2lem4  33556  cycpmco2lem5  33557  cycpmco2lem6  33558  cycpmco2  33560  archirngz  33616  archiabllem1a  33618  archiabllem1  33620  archiabllem2c  33622  constrrtcc  34232  cos9thpiminplylem1  34279  cos9thpiminplylem2  34280  cos9thpiminplylem3  34281  cos9thpinconstrlem1  34286  ballotlemsdom  35010  fsum2dsub  35102  resconn  35812  iprodgam  36308  faclimlem1  36309  faclimlem3  36311  faclim  36312  iprodfac  36313  fwddifnp1  36732  dnibndlem7  37168  dnibndlem8  37169  knoppndvlem14  37209  bj-bary1  38051  dvtan  38406  itgaddnclem2  38415  itgmulc2nc  38424  ftc1anclem8  38436  dvasin  38440  areacirclem1  38444  lcmineqlem19  42900  aks4d1p1p2  42923  posbezout  42953  sticksstones7  43005  sticksstones12a  43010  sticksstones12  43011  bcle2d  43032  aks6d1c7lem1  43033  quadfac  43058  dffltz  43467  fltbccoprm  43474  flt4lem3  43481  flt4lem5c  43487  flt4lem5d  43488  flt4lem5e  43489  flt4lem7  43492  nna4b4nsq  43493  fltnltalem  43495  3cubeslem2  43517  3cubeslem3l  43518  3cubeslem3r  43519  pellexlem2  43658  pell14qrgt0  43687  rmxyadd  43749  rmxluc  43764  fzmaxdif  43809  acongeq  43811  jm2.19lem2  43818  jm2.26lem3  43829  areaquad  44044  sqrtcval  44468  int-addcomd  45000  int-leftdistd  45006  subadd4b  46103  sub31  46110  coseq0  46679  coskpi2  46681  cosknegpi  46684  fperdvper  46734  dvbdfbdioolem2  46744  dvnmul  46758  dvmptfprodlem  46759  itgsincmulx  46789  itgsbtaddcnst  46797  stoweidlem11  46826  stirlinglem5  46893  stirlinglem7  46895  dirkertrigeqlem1  46913  dirkertrigeqlem2  46914  dirkertrigeqlem3  46915  dirkertrigeq  46916  dirkercncflem2  46919  fourierdlem4  46926  fourierdlem26  46948  fourierdlem40  46962  fourierdlem42  46964  fourierdlem47  46968  fourierdlem63  46984  fourierdlem64  46985  fourierdlem65  46986  fourierdlem74  46995  fourierdlem75  46996  fourierdlem78  46999  fourierdlem79  47000  fourierdlem84  47005  fourierdlem93  47014  fourierdlem103  47024  fourierdlem111  47032  fourierswlem  47045  fouriersw  47046  etransclem32  47081  etransclem46  47095  sge0gtfsumgt  47258  hoidmv1lelem2  47407  hoidmvlelem2  47411  hspmbllem1  47441  smfmullem1  47606  sigarperm  47675  sin5tlem1  47724  sin5tlem5  47728  cjnpoly  47744  2elfz2melfz  48193  m1modmmod  48239  mod2addne  48245  fargshiftfo  48329  ichexmpl2  48357  fmtnorec3  48438  2zrngacmnd  49150  2zrngagrp  49151  ply1mulgsumlem1  49303  ackval1  49598  ackval2  49599  resum2sqorgt0  49626  eenglngeehlnmlem2  49655  rrx2linest2  49661  line2xlem  49670  itsclc0yqsollem1  49679  itsclc0yqsol  49681  itscnhlc0xyqsol  49682  itsclc0xyqsolr  49686  itsclinecirc0b  49691  itsclquadb  49693  2itscplem1  49695  2itscp  49698  onetansqsecsq  50674  crossp3d  50787