Theorem addcomd 8323

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  (class class class)co 6013  ℂcc 8023   + caddc 8028

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

This theorem is referenced by:  muladd11r  8328  comraddd  8329  subadd2  8376  pncan  8378  npcan  8381  subcan  8427  mvlladdd  8537  subaddeqd  8541  addrsub  8543  ltadd1  8602  leadd2  8604  ltsubadd2  8606  lesubadd2  8608  mulreim  8777  apadd2  8782  recp1lt1  9072  ltaddrp2d  9959  lincmb01cmp  10231  iccf1o  10232  elfzoext  10430  rebtwn2zlemstep  10505  qavgle  10511  modqaddabs  10617  mulqaddmodid  10619  qnegmod  10624  modqadd2mod  10629  modqadd12d  10635  modqaddmulmod  10646  addmodlteq  10653  expaddzap  10838  bcn2m1  11024  bcn2p1  11025  lenrevpfxcctswrd  11286  remullem  11425  resqrexlemover  11564  maxabslemab  11760  maxabslemval  11762  bdtrilem  11793  climaddc2  11884  telfsumo  12020  fsumparts  12024  bcxmas  12043  isumshft  12044  cvgratnnlemsumlt  12082  cosneg  12281  sinadd  12290  sincossq  12302  cos2t  12304  absefi  12323  absefib  12325  gcdaddm  12548  pythagtrip  12849  pcadd2  12907  mulgnndir  13731  mulgdirlem  13733  metrtri  15094  plymullem1  15465  lgseisenlem1  15792  2sqlem3  15839  apdifflemf  16600  apdiff  16602