Theorem addcomd 8373

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 8359	. 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 2202  (class class class)co 6028   CCcc 8073   + caddc 8078

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

This theorem is referenced by:  muladd11r  8378  comraddd  8379  subadd2  8426  pncan  8428  npcan  8431  subcan  8477  mvlladdd  8587  subaddeqd  8591  addrsub  8593  ltadd1  8652  leadd2  8654  ltsubadd2  8656  lesubadd2  8658  mulreim  8827  apadd2  8832  recp1lt1  9122  ltaddrp2d  10009  lincmb01cmp  10281  iccf1o  10282  elfzoext  10481  rebtwn2zlemstep  10556  qavgle  10562  modqaddabs  10668  mulqaddmodid  10670  qnegmod  10675  modqadd2mod  10680  modqadd12d  10686  modqaddmulmod  10697  addmodlteq  10704  expaddzap  10889  bcn2m1  11075  bcn2p1  11076  lenrevpfxcctswrd  11340  remullem  11492  resqrexlemover  11631  maxabslemab  11827  maxabslemval  11829  bdtrilem  11860  climaddc2  11951  telfsumo  12088  fsumparts  12092  bcxmas  12111  isumshft  12112  cvgratnnlemsumlt  12150  cosneg  12349  sinadd  12358  sincossq  12370  cos2t  12372  absefi  12391  absefib  12393  gcdaddm  12616  pythagtrip  12917  pcadd2  12975  mulgnndir  13799  mulgdirlem  13801  metrtri  15168  plymullem1  15539  pellexlem2  15772  lgseisenlem1  15869  2sqlem3  15916  eupth2lem3lem3fi  16391  apdifflemf  16758  apdiff  16760