Theorem addcomd 8335

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	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcomd.2	⊢ (𝜑 → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
addcomd	⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Proof of Theorem addcomd

Step	Hyp	Ref	Expression
1		muld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcomd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		addcom 8321	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2201  (class class class)co 6023  ℂcc 8035   + caddc 8040

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

This theorem is referenced by:  muladd11r  8340  comraddd  8341  subadd2  8388  pncan  8390  npcan  8393  subcan  8439  mvlladdd  8549  subaddeqd  8553  addrsub  8555  ltadd1  8614  leadd2  8616  ltsubadd2  8618  lesubadd2  8620  mulreim  8789  apadd2  8794  recp1lt1  9084  ltaddrp2d  9971  lincmb01cmp  10243  iccf1o  10244  elfzoext  10443  rebtwn2zlemstep  10518  qavgle  10524  modqaddabs  10630  mulqaddmodid  10632  qnegmod  10637  modqadd2mod  10642  modqadd12d  10648  modqaddmulmod  10659  addmodlteq  10666  expaddzap  10851  bcn2m1  11037  bcn2p1  11038  lenrevpfxcctswrd  11302  remullem  11454  resqrexlemover  11593  maxabslemab  11789  maxabslemval  11791  bdtrilem  11822  climaddc2  11913  telfsumo  12050  fsumparts  12054  bcxmas  12073  isumshft  12074  cvgratnnlemsumlt  12112  cosneg  12311  sinadd  12320  sincossq  12332  cos2t  12334  absefi  12353  absefib  12355  gcdaddm  12578  pythagtrip  12879  pcadd2  12937  mulgnndir  13761  mulgdirlem  13763  metrtri  15130  plymullem1  15501  lgseisenlem1  15828  2sqlem3  15875  eupth2lem3lem3fi  16350  apdifflemf  16717  apdiff  16719