Theorem addcomd 8106

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 8092	. 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 5874   CCcc 7808   + caddc 7813

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

This theorem is referenced by:  muladd11r  8111  comraddd  8112  subadd2  8159  pncan  8161  npcan  8164  subcan  8210  mvlladdd  8320  subaddeqd  8324  addrsub  8326  ltadd1  8384  leadd2  8386  ltsubadd2  8388  lesubadd2  8390  mulreim  8559  apadd2  8564  recp1lt1  8854  ltaddrp2d  9729  lincmb01cmp  10001  iccf1o  10002  rebtwn2zlemstep  10250  qavgle  10256  modqaddabs  10359  mulqaddmodid  10361  qnegmod  10366  modqadd2mod  10371  modqadd12d  10377  modqaddmulmod  10388  addmodlteq  10395  expaddzap  10561  bcn2m1  10744  bcn2p1  10745  remullem  10875  resqrexlemover  11014  maxabslemab  11210  maxabslemval  11212  bdtrilem  11242  climaddc2  11333  telfsumo  11469  fsumparts  11473  bcxmas  11492  isumshft  11493  cvgratnnlemsumlt  11531  cosneg  11730  sinadd  11739  sincossq  11751  cos2t  11753  absefi  11771  absefib  11773  gcdaddm  11979  pythagtrip  12277  mulgnndir  12965  mulgdirlem  12967  metrtri  13770  2sqlem3  14346  apdifflemf  14676  apdiff  14678