Theorem addcomd 8440

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 8426	. 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 2205  (class class class)co 6058   CCcc 8141   + caddc 8146

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

This theorem is referenced by:  muladd11r  8445  comraddd  8446  subadd2  8493  pncan  8495  npcan  8498  subcan  8544  mvlladdd  8654  subaddeqd  8658  addrsub  8660  ltadd1  8720  leadd2  8722  ltsubadd2  8724  lesubadd2  8726  mulreim  8895  apadd2  8900  recp1lt1  9190  ltaddrp2d  10082  lincmb01cmp  10355  iccf1o  10357  elfzoext  10559  rebtwn2zlemstep  10636  qavgle  10642  modqaddabs  10748  mulqaddmodid  10750  qnegmod  10755  modqadd2mod  10760  modqadd12d  10766  modqaddmulmod  10777  addmodlteq  10784  expaddzap  10969  bcn2m1  11157  bcn2p1  11158  lenrevpfxcctswrd  11429  remullem  11581  resqrexlemover  11720  maxabslemab  11916  maxabslemval  11918  bdtrilem  11949  climaddc2  12040  telfsumo  12177  fsumparts  12181  bcxmas  12200  isumshft  12201  cvgratnnlemsumlt  12239  cosneg  12438  sinadd  12447  sincossq  12459  cos2t  12461  absefi  12480  absefib  12482  gcdaddm  12705  pythagtrip  13006  pcadd2  13064  ballotfilemsdom  13199  mulgnndir  13952  mulgdirlem  13954  metrtri  15354  plymullem1  15725  pellexlem2  15958  lgseisenlem1  16055  2sqlem3  16102  eupth2lem3lem3fi  16577  apdifflemf  16942  apdiff  16944