Theorem addcomd 7623

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

Syntax hints:   -> wi 4   = wceq 1289   e. wcel 1438  (class class class)co 5644   CCcc 7338   + caddc 7343

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

This theorem is referenced by:  muladd11r  7628  comraddd  7629  subadd2  7676  pncan  7678  npcan  7681  subcan  7727  subaddeqd  7837  addrsub  7839  ltadd1  7897  leadd2  7899  ltsubadd2  7901  lesubadd2  7903  mulreim  8071  apadd2  8076  recp1lt1  8350  ltaddrp2d  9198  lincmb01cmp  9410  iccf1o  9411  rebtwn2zlemstep  9652  qavgle  9658  modqaddabs  9757  mulqaddmodid  9759  qnegmod  9764  modqadd2mod  9769  modqadd12d  9775  modqaddmulmod  9786  addmodlteq  9793  expaddzap  9987  bcn2m1  10165  bcn2p1  10166  remullem  10293  resqrexlemover  10431  maxabslemab  10627  maxabslemval  10629  climaddc2  10705  telfsumo  10847  fsumparts  10851  bcxmas  10870  isumshft  10871  cvgratnnlemsumlt  10909  cosneg  11005  sinadd  11014  sincossq  11026  cos2t  11028  absefi  11045  absefib  11047  gcdaddm  11240