Theorem addcomd 8330

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 8316	. 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 1397   e. wcel 2202  (class class class)co 6018   CCcc 8030   + caddc 8035

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

This theorem is referenced by:  muladd11r  8335  comraddd  8336  subadd2  8383  pncan  8385  npcan  8388  subcan  8434  mvlladdd  8544  subaddeqd  8548  addrsub  8550  ltadd1  8609  leadd2  8611  ltsubadd2  8613  lesubadd2  8615  mulreim  8784  apadd2  8789  recp1lt1  9079  ltaddrp2d  9966  lincmb01cmp  10238  iccf1o  10239  elfzoext  10438  rebtwn2zlemstep  10513  qavgle  10519  modqaddabs  10625  mulqaddmodid  10627  qnegmod  10632  modqadd2mod  10637  modqadd12d  10643  modqaddmulmod  10654  addmodlteq  10661  expaddzap  10846  bcn2m1  11032  bcn2p1  11033  lenrevpfxcctswrd  11297  remullem  11436  resqrexlemover  11575  maxabslemab  11771  maxabslemval  11773  bdtrilem  11804  climaddc2  11895  telfsumo  12032  fsumparts  12036  bcxmas  12055  isumshft  12056  cvgratnnlemsumlt  12094  cosneg  12293  sinadd  12302  sincossq  12314  cos2t  12316  absefi  12335  absefib  12337  gcdaddm  12560  pythagtrip  12861  pcadd2  12919  mulgnndir  13743  mulgdirlem  13745  metrtri  15107  plymullem1  15478  lgseisenlem1  15805  2sqlem3  15852  eupth2lem3lem3fi  16327  apdifflemf  16676  apdiff  16678