Theorem addcomd 8194

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167  (class class class)co 5925  ℂcc 7894   + caddc 7899

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

This theorem is referenced by:  muladd11r  8199  comraddd  8200  subadd2  8247  pncan  8249  npcan  8252  subcan  8298  mvlladdd  8408  subaddeqd  8412  addrsub  8414  ltadd1  8473  leadd2  8475  ltsubadd2  8477  lesubadd2  8479  mulreim  8648  apadd2  8653  recp1lt1  8943  ltaddrp2d  9823  lincmb01cmp  10095  iccf1o  10096  rebtwn2zlemstep  10359  qavgle  10365  modqaddabs  10471  mulqaddmodid  10473  qnegmod  10478  modqadd2mod  10483  modqadd12d  10489  modqaddmulmod  10500  addmodlteq  10507  expaddzap  10692  bcn2m1  10878  bcn2p1  10879  remullem  11053  resqrexlemover  11192  maxabslemab  11388  maxabslemval  11390  bdtrilem  11421  climaddc2  11512  telfsumo  11648  fsumparts  11652  bcxmas  11671  isumshft  11672  cvgratnnlemsumlt  11710  cosneg  11909  sinadd  11918  sincossq  11930  cos2t  11932  absefi  11951  absefib  11953  gcdaddm  12176  pythagtrip  12477  pcadd2  12535  mulgnndir  13357  mulgdirlem  13359  metrtri  14697  plymullem1  15068  lgseisenlem1  15395  2sqlem3  15442  apdifflemf  15777  apdiff  15779