Theorem addcomd 8177

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 8163	. 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 1364   e. wcel 2167  (class class class)co 5922   CCcc 7877   + caddc 7882

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

This theorem is referenced by:  muladd11r  8182  comraddd  8183  subadd2  8230  pncan  8232  npcan  8235  subcan  8281  mvlladdd  8391  subaddeqd  8395  addrsub  8397  ltadd1  8456  leadd2  8458  ltsubadd2  8460  lesubadd2  8462  mulreim  8631  apadd2  8636  recp1lt1  8926  ltaddrp2d  9806  lincmb01cmp  10078  iccf1o  10079  rebtwn2zlemstep  10342  qavgle  10348  modqaddabs  10454  mulqaddmodid  10456  qnegmod  10461  modqadd2mod  10466  modqadd12d  10472  modqaddmulmod  10483  addmodlteq  10490  expaddzap  10675  bcn2m1  10861  bcn2p1  10862  remullem  11036  resqrexlemover  11175  maxabslemab  11371  maxabslemval  11373  bdtrilem  11404  climaddc2  11495  telfsumo  11631  fsumparts  11635  bcxmas  11654  isumshft  11655  cvgratnnlemsumlt  11693  cosneg  11892  sinadd  11901  sincossq  11913  cos2t  11915  absefi  11934  absefib  11936  gcdaddm  12151  pythagtrip  12452  pcadd2  12510  mulgnndir  13281  mulgdirlem  13283  metrtri  14613  plymullem1  14984  lgseisenlem1  15311  2sqlem3  15358  apdifflemf  15690  apdiff  15692