Theorem addcomd 8441

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 8427	. 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  8446  comraddd  8447  subadd2  8494  pncan  8496  npcan  8499  subcan  8545  mvlladdd  8655  subaddeqd  8659  addrsub  8661  ltadd1  8721  leadd2  8723  ltsubadd2  8725  lesubadd2  8727  mulreim  8896  apadd2  8901  recp1lt1  9193  ltaddrp2d  10085  lincmb01cmp  10358  iccf1o  10360  elfzoext  10562  rebtwn2zlemstep  10639  qavgle  10645  modqaddabs  10751  mulqaddmodid  10753  qnegmod  10758  modqadd2mod  10763  modqadd12d  10769  modqaddmulmod  10780  addmodlteq  10787  expaddzap  10972  bcn2m1  11160  bcn2p1  11161  lenrevpfxcctswrd  11432  remullem  11584  resqrexlemover  11724  maxabslemab  11920  maxabslemval  11922  bdtrilem  11953  climaddc2  12044  telfsumo  12181  fsumparts  12185  bcxmas  12204  isumshft  12205  cvgratnnlemsumlt  12243  cosneg  12442  sinadd  12451  sincossq  12463  cos2t  12465  absefi  12484  absefib  12486  gcdaddm  12709  pythagtrip  13010  pcadd2  13068  ballotfilemsdom  13203  mulgnndir  13908  mulgdirlem  13910  metrtri  15372  plymullem1  15743  pellexlem2  15976  lgseisenlem1  16073  2sqlem3  16120  eupth2lem3lem3fi  16595  apdifflemf  16970  apdiff  16972