Theorem addcomd 8479

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 8465	. 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 6085   CCcc 8178   + caddc 8183

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

This theorem is used by:  muladd11r  8484  comraddd  8485  subadd2  8532  pncan  8534  npcan  8537  subcan  8583  mvlladdd  8693  subaddeqd  8697  addrsub  8699  ltadd1  8759  leadd2  8761  ltsubadd2  8763  lesubadd2  8765  lesub3d  8893  mulreim  8935  apadd2  8940  recp1lt1  9232  ltaddrp2d  10143  lincmb01cmp  10416  iccf1o  10418  elfzoext  10621  rebtwn2zlemstep  10698  qavgle  10704  modqaddabs  10813  mulqaddmodid  10815  qnegmod  10820  modqadd2mod  10825  modqadd12d  10831  modqaddmulmod  10842  addmodlteq  10849  expaddzap  11034  bcn2m1  11223  bcn2p1  11224  lenrevpfxcctswrd  11499  remullem  11651  resqrexlemover  11791  maxabslemab  11988  maxabslemval  11990  bdtrilem  12023  climaddc2  12114  telfsumo  12251  fsumparts  12255  bcxmas  12274  isumshft  12275  cvgratnnlemsumlt  12313  cosneg  12512  sinadd  12521  sincossq  12533  cos2t  12535  absefi  12554  absefib  12556  gcdaddm  12779  pythagtrip  13084  pcadd2  13142  ballotfilemsdom  13306  mulgnndir  14005  mulgdirlem  14007  metrtri  15530  plymullem1  15901  efap1p  15932  pellexlem2  16152  lgseisenlem1  16311  2sqlem3  16358  eupth2lem3lem3fi  16833  apdifflemf  17217  apdiff  17219