Theorem addcomd 8318

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 8304	. 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 6011   CCcc 8018   + caddc 8023

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

This theorem is referenced by:  muladd11r  8323  comraddd  8324  subadd2  8371  pncan  8373  npcan  8376  subcan  8422  mvlladdd  8532  subaddeqd  8536  addrsub  8538  ltadd1  8597  leadd2  8599  ltsubadd2  8601  lesubadd2  8603  mulreim  8772  apadd2  8777  recp1lt1  9067  ltaddrp2d  9954  lincmb01cmp  10226  iccf1o  10227  elfzoext  10425  rebtwn2zlemstep  10500  qavgle  10506  modqaddabs  10612  mulqaddmodid  10614  qnegmod  10619  modqadd2mod  10624  modqadd12d  10630  modqaddmulmod  10641  addmodlteq  10648  expaddzap  10833  bcn2m1  11019  bcn2p1  11020  lenrevpfxcctswrd  11280  remullem  11419  resqrexlemover  11558  maxabslemab  11754  maxabslemval  11756  bdtrilem  11787  climaddc2  11878  telfsumo  12014  fsumparts  12018  bcxmas  12037  isumshft  12038  cvgratnnlemsumlt  12076  cosneg  12275  sinadd  12284  sincossq  12296  cos2t  12298  absefi  12317  absefib  12319  gcdaddm  12542  pythagtrip  12843  pcadd2  12901  mulgnndir  13725  mulgdirlem  13727  metrtri  15088  plymullem1  15459  lgseisenlem1  15786  2sqlem3  15833  apdifflemf  16560  apdiff  16562