Theorem addcomd 8122

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 8108	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   = wceq 1363   ∈ wcel 2158  (class class class)co 5888  ℂcc 7823   + caddc 7828

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

This theorem is referenced by:  muladd11r  8127  comraddd  8128  subadd2  8175  pncan  8177  npcan  8180  subcan  8226  mvlladdd  8336  subaddeqd  8340  addrsub  8342  ltadd1  8400  leadd2  8402  ltsubadd2  8404  lesubadd2  8406  mulreim  8575  apadd2  8580  recp1lt1  8870  ltaddrp2d  9745  lincmb01cmp  10017  iccf1o  10018  rebtwn2zlemstep  10267  qavgle  10273  modqaddabs  10376  mulqaddmodid  10378  qnegmod  10383  modqadd2mod  10388  modqadd12d  10394  modqaddmulmod  10405  addmodlteq  10412  expaddzap  10578  bcn2m1  10763  bcn2p1  10764  remullem  10894  resqrexlemover  11033  maxabslemab  11229  maxabslemval  11231  bdtrilem  11261  climaddc2  11352  telfsumo  11488  fsumparts  11492  bcxmas  11511  isumshft  11512  cvgratnnlemsumlt  11550  cosneg  11749  sinadd  11758  sincossq  11770  cos2t  11772  absefi  11790  absefib  11792  gcdaddm  11999  pythagtrip  12297  mulgnndir  13044  mulgdirlem  13046  metrtri  14173  lgseisenlem1  14746  2sqlem3  14760  apdifflemf  15091  apdiff  15093