Theorem addcomd 8485

Description: Addition is commutative. 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 8471	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
4	1, 2, 3	syl2anc 415	1 |- ( ph -> ( A + B ) = ( B + A ) )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209  (class class class)co 6088   CCcc 8184   + caddc 8189

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-addcom 8286

This theorem is used by:  muladd11r  8490  comraddd  8491  subadd2  8538  pncan  8540  npcan  8543  subcan  8589  mvlladdd  8699  subaddeqd  8703  addrsub  8705  ltadd1  8765  leadd2  8767  ltsubadd2  8769  lesubadd2  8771  lesub3d  8899  mulreim  8941  apadd2  8946  recp1lt1  9238  ltaddrp2d  10149  lincmb01cmp  10422  iccf1o  10424  elfzoext  10627  rebtwn2zlemstep  10704  qavgle  10710  modqaddabs  10820  mulqaddmodid  10822  qnegmod  10827  modqadd2mod  10832  modqadd12d  10838  modqaddmulmod  10849  addmodlteq  10856  expaddzap  11041  bcn2m1  11230  bcn2p1  11231  lenrevpfxcctswrd  11506  remullem  11658  resqrexlemover  11798  maxabslemab  11995  maxabslemval  11997  bdtrilem  12030  climaddc2  12121  telfsumo  12258  fsumparts  12262  bcxmas  12281  isumshft  12282  cvgratnnlemsumlt  12320  cosneg  12519  sinadd  12528  sincossq  12540  cos2t  12542  absefi  12561  absefib  12563  gcdaddm  12786  pythagtrip  13091  pcadd2  13149  ballotfilemsdom  13313  mulgnndir  14013  mulgdirlem  14015  metrtri  15636  plymullem1  16007  efap1p  16038  pellexlem2  16263  bposlem9  16352  lgseisenlem1  16427  2sqlem3  16474  eupth2lem3lem3fi  16949  apdifflemf  17335  apdiff  17337