Theorem addcomd 8285

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 8271	. 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 1395   e. wcel 2200  (class class class)co 5994   CCcc 7985   + caddc 7990

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

This theorem is referenced by:  muladd11r  8290  comraddd  8291  subadd2  8338  pncan  8340  npcan  8343  subcan  8389  mvlladdd  8499  subaddeqd  8503  addrsub  8505  ltadd1  8564  leadd2  8566  ltsubadd2  8568  lesubadd2  8570  mulreim  8739  apadd2  8744  recp1lt1  9034  ltaddrp2d  9915  lincmb01cmp  10187  iccf1o  10188  elfzoext  10385  rebtwn2zlemstep  10459  qavgle  10465  modqaddabs  10571  mulqaddmodid  10573  qnegmod  10578  modqadd2mod  10583  modqadd12d  10589  modqaddmulmod  10600  addmodlteq  10607  expaddzap  10792  bcn2m1  10978  bcn2p1  10979  lenrevpfxcctswrd  11230  remullem  11368  resqrexlemover  11507  maxabslemab  11703  maxabslemval  11705  bdtrilem  11736  climaddc2  11827  telfsumo  11963  fsumparts  11967  bcxmas  11986  isumshft  11987  cvgratnnlemsumlt  12025  cosneg  12224  sinadd  12233  sincossq  12245  cos2t  12247  absefi  12266  absefib  12268  gcdaddm  12491  pythagtrip  12792  pcadd2  12850  mulgnndir  13674  mulgdirlem  13676  metrtri  15036  plymullem1  15407  lgseisenlem1  15734  2sqlem3  15781  apdifflemf  16345  apdiff  16347