MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addcomd Unicode version

Theorem addcomd 9803
Description: Addition commutes. 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
StepHypRef Expression
1 1cnd 9633 . . . . . . . 8
21, 1addcld 9636 . . . . . . 7
3 muld.1 . . . . . . 7
4 addcomd.2 . . . . . . 7
52, 3, 4adddid 9641 . . . . . 6
63, 4addcld 9636 . . . . . . 7
7 1p1times 9772 . . . . . . 7
86, 7syl 16 . . . . . 6
9 1p1times 9772 . . . . . . . 8
103, 9syl 16 . . . . . . 7
11 1p1times 9772 . . . . . . . 8
124, 11syl 16 . . . . . . 7
1310, 12oveq12d 6314 . . . . . 6
145, 8, 133eqtr3rd 2507 . . . . 5
153, 3addcld 9636 . . . . . 6
1615, 4, 4addassd 9639 . . . . 5
176, 3, 4addassd 9639 . . . . 5
1814, 16, 173eqtr4d 2508 . . . 4
1915, 4addcld 9636 . . . . 5
206, 3addcld 9636 . . . . 5
21 addcan2 9786 . . . . 5
2219, 20, 4, 21syl3anc 1228 . . . 4
2318, 22mpbid 210 . . 3
243, 3, 4addassd 9639 . . 3
253, 4, 3addassd 9639 . . 3
2623, 24, 253eqtr3d 2506 . 2
274, 3addcld 9636 . . 3
28 addcan 9785 . . 3
293, 6, 27, 28syl3anc 1228 . 2
3026, 29mpbid 210 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818  (class class class)co 6296   cc 9511  1c1 9514   caddc 9516   cmul 9518
This theorem is referenced by:  subadd2  9847  pncan  9849  npcan  9852  subcan  9897  ltadd1  10044  leadd2  10046  ltsubadd2  10048  lesubadd2  10050  ltaddrp2d  11315  lincmb01cmp  11692  iccf1o  11693  modaddabs  12034  modadd2mod  12037  modadd12d  12043  modaddmulmod  12053  expaddz  12210  bcn2m1  12402  bcn2p1  12403  ccatrn  12606  addlenswrd  12662  spllen  12730  splfv2a  12732  remullem  12961  sqreulem  13192  climaddc2  13458  clim2ser2  13478  iseraltlem2  13505  telfsumo  13616  fsumparts  13620  bcxmas  13647  cosneg  13882  coshval  13890  sinadd  13899  sincossq  13911  cos2t  13913  absefi  13931  absefib  13933  sadadd2lem2  14100  bitsres  14123  bezoutlem2  14177  bezoutlem4  14179  pythagtrip  14358  pcadd2  14409  vdwapun  14492  vdwlem5  14503  vdwlem6  14504  vdwlem8  14506  gsumccat  16009  mulgnndir  16164  mulgdirlem  16166  mulgdir  16167  sylow1lem1  16618  efgcpbllemb  16773  cygabl  16893  ablfacrp  17117  icccvx  21450  pjthlem1  21852  ovolicc2lem4  21931  cmmbl  21945  voliunlem1  21960  itgmulc2  22240  dvle  22408  dvcvx  22421  dvfsumlem2  22428  dvfsumlem4  22430  dvfsum2  22435  ply1divex  22537  plymullem1  22611  coeeulem  22621  aaliou3lem6  22744  dvtaylp  22765  ulmcn  22794  abelthlem7  22833  pilem3  22848  rzgrp  22941  lawcos  23148  affineequiv  23157  heron  23169  quad2  23170  dcubic1lem  23174  dcubic2  23175  dcubic  23177  mcubic  23178  quart1lem  23186  quart1  23187  asinlem2  23200  asinsin  23223  cosasin  23235  atanlogaddlem  23244  atanlogadd  23245  cvxcl  23314  scvxcvx  23315  bposlem9  23567  lgseisenlem1  23624  2sqlem3  23641  2sqblem  23652  dchrisumlem2  23675  selberg  23733  selberg2  23736  chpdifbndlem1  23738  selberg4  23746  pntrlog2bndlem1  23762  pntrlog2bndlem6  23768  pntibndlem2  23776  pntlemb  23782  pntlemf  23790  padicabv  23815  colinearalglem2  24210  axsegconlem9  24228  axpasch  24244  axeuclidlem  24265  cusgrasizeinds  24476  fargshiftfo  24638  eupath2lem3  24979  numclwlk3lem3  25073  smcnlem  25607  ipval2  25617  hhph  26095  pjhthlem1  26309  golem1  27190  stcltrlem1  27195  addeqxfrd  27560  bhmafibid2  27633  2sqmod  27636  omndmul2  27702  archirngz  27733  archiabllem1a  27735  archiabllem1  27737  archiabllem2c  27739  ballotlemsdom  28450  signshf  28545  lgamgulmlem2  28572  lgamgulmlem3  28573  lgamcvg2  28597  lgam1  28606  rescon  28691  rtrclreclem.trans  29069  iprodgam  29125  faclimlem1  29168  faclimlem3  29170  faclim  29171  iprodfac  29172  bpoly4  29821  supadd  30042  dvtan  30065  itg2addnclem3  30068  itgaddnclem2  30074  itgmulc2nc  30083  ftc1anclem8  30097  dvasin  30103  areacirclem1  30107  pellexlem2  30766  pell14qrgt0  30795  rmxyadd  30857  rmxluc  30872  fzmaxdif  30919  acongeq  30921  jm2.19lem2  30932  jm2.26lem3  30943  areaquad  31184  subadd4b  31464  sub31  31479  fsumsplit1  31573  coseq0  31664  coskpi2  31666  cosknegpi  31669  fperdvper  31715  dvbdfbdioolem2  31726  dvnmul  31740  dvmptfprodlem  31741  itgsincmulx  31773  itgsbtaddcnst  31781  stoweidlem11  31793  stirlinglem5  31860  stirlinglem7  31862  dirkertrigeqlem1  31880  dirkertrigeqlem2  31881  dirkertrigeqlem3  31882  dirkertrigeq  31883  dirkercncflem2  31886  fourierdlem4  31893  fourierdlem26  31915  fourierdlem40  31929  fourierdlem42  31931  fourierdlem47  31936  fourierdlem63  31952  fourierdlem64  31953  fourierdlem65  31954  fourierdlem74  31963  fourierdlem75  31964  fourierdlem78  31967  fourierdlem79  31968  fourierdlem84  31973  fourierdlem93  31982  fourierdlem103  31992  fourierdlem111  32000  fourierswlem  32013  fouriersw  32014  etransclem32  32049  etransclem46  32063  sigarperm  32077  2elfz2melfz  32334  2zrngacmnd  32748  2zrngagrp  32749  ply1mulgsumlem1  32986  onetansqsecsq  33155  comraddd  33176  mvlladdd  33178  bj-rsub  34672  bj-bary1  34681  int-addcomd  37994  int-leftdistd  38000
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-mulcom 9577  ax-addass 9578  ax-mulass 9579  ax-distr 9580  ax-i2m1 9581  ax-1ne0 9582  ax-1rid 9583  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586  ax-pre-lttri 9587  ax-pre-lttrn 9588  ax-pre-ltadd 9589
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-po 4805  df-so 4806  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-ov 6299  df-er 7330  df-en 7537  df-dom 7538  df-sdom 7539  df-pnf 9651  df-mnf 9652  df-ltxr 9654
  Copyright terms: Public domain W3C validator