Theorem addcomd 8423

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	|- ( ph -> A e. CC )
addcomd.2	|- ( ph -> B e. CC )

Assertion

Ref	Expression
addcomd	|- ( ph -> ( A + B ) = ( B + A ) )

Proof of Theorem addcomd

Step	Hyp	Ref	Expression
1		muld.1	. 2 |- ( ph -> A e. CC )
2		addcomd.2	. 2 |- ( ph -> B e. CC )
3		addcom 8409	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
4	1, 2, 3	syl2anc 411	1 |- ( ph -> ( A + B ) = ( B + A ) )

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2203  (class class class)co 6049   CCcc 8124   + caddc 8129

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-addcom 8226

This theorem is referenced by:  muladd11r  8428  comraddd  8429  subadd2  8476  pncan  8478  npcan  8481  subcan  8527  mvlladdd  8637  subaddeqd  8641  addrsub  8643  ltadd1  8702  leadd2  8704  ltsubadd2  8706  lesubadd2  8708  mulreim  8877  apadd2  8882  recp1lt1  9172  ltaddrp2d  10063  lincmb01cmp  10335  iccf1o  10337  elfzoext  10536  rebtwn2zlemstep  10611  qavgle  10617  modqaddabs  10723  mulqaddmodid  10725  qnegmod  10730  modqadd2mod  10735  modqadd12d  10741  modqaddmulmod  10752  addmodlteq  10759  expaddzap  10944  bcn2m1  11130  bcn2p1  11131  lenrevpfxcctswrd  11400  remullem  11552  resqrexlemover  11691  maxabslemab  11887  maxabslemval  11889  bdtrilem  11920  climaddc2  12011  telfsumo  12148  fsumparts  12152  bcxmas  12171  isumshft  12172  cvgratnnlemsumlt  12210  cosneg  12409  sinadd  12418  sincossq  12430  cos2t  12432  absefi  12451  absefib  12453  gcdaddm  12676  pythagtrip  12977  pcadd2  13035  mulgnndir  13860  mulgdirlem  13862  metrtri  15234  plymullem1  15605  pellexlem2  15838  lgseisenlem1  15935  2sqlem3  15982  eupth2lem3lem3fi  16457  apdifflemf  16822  apdiff  16824