Theorem addcomd 7913

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 7899	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
4	1, 2, 3	syl2anc 408	1 |- ( ph -> ( A + B ) = ( B + A ) )

Syntax hints:   -> wi 4   = wceq 1331   e. wcel 1480  (class class class)co 5774   CCcc 7618   + caddc 7623

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

This theorem is referenced by:  muladd11r  7918  comraddd  7919  subadd2  7966  pncan  7968  npcan  7971  subcan  8017  mvlladdd  8127  subaddeqd  8131  addrsub  8133  ltadd1  8191  leadd2  8193  ltsubadd2  8195  lesubadd2  8197  mulreim  8366  apadd2  8371  recp1lt1  8657  ltaddrp2d  9518  lincmb01cmp  9786  iccf1o  9787  rebtwn2zlemstep  10030  qavgle  10036  modqaddabs  10135  mulqaddmodid  10137  qnegmod  10142  modqadd2mod  10147  modqadd12d  10153  modqaddmulmod  10164  addmodlteq  10171  expaddzap  10337  bcn2m1  10515  bcn2p1  10516  remullem  10643  resqrexlemover  10782  maxabslemab  10978  maxabslemval  10980  bdtrilem  11010  climaddc2  11099  telfsumo  11235  fsumparts  11239  bcxmas  11258  isumshft  11259  cvgratnnlemsumlt  11297  cosneg  11434  sinadd  11443  sincossq  11455  cos2t  11457  absefi  11475  absefib  11477  gcdaddm  11672  metrtri  12546