Theorem addcomd 8110

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 8096	. 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 1353   e. wcel 2148  (class class class)co 5877   CCcc 7811   + caddc 7816

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

This theorem is referenced by:  muladd11r  8115  comraddd  8116  subadd2  8163  pncan  8165  npcan  8168  subcan  8214  mvlladdd  8324  subaddeqd  8328  addrsub  8330  ltadd1  8388  leadd2  8390  ltsubadd2  8392  lesubadd2  8394  mulreim  8563  apadd2  8568  recp1lt1  8858  ltaddrp2d  9733  lincmb01cmp  10005  iccf1o  10006  rebtwn2zlemstep  10255  qavgle  10261  modqaddabs  10364  mulqaddmodid  10366  qnegmod  10371  modqadd2mod  10376  modqadd12d  10382  modqaddmulmod  10393  addmodlteq  10400  expaddzap  10566  bcn2m1  10751  bcn2p1  10752  remullem  10882  resqrexlemover  11021  maxabslemab  11217  maxabslemval  11219  bdtrilem  11249  climaddc2  11340  telfsumo  11476  fsumparts  11480  bcxmas  11499  isumshft  11500  cvgratnnlemsumlt  11538  cosneg  11737  sinadd  11746  sincossq  11758  cos2t  11760  absefi  11778  absefib  11780  gcdaddm  11987  pythagtrip  12285  mulgnndir  13017  mulgdirlem  13019  metrtri  13916  lgseisenlem1  14489  2sqlem3  14503  apdifflemf  14833  apdiff  14835