Theorem addcomd 8045

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

Syntax hints:   → wi 4   = wceq 1343   ∈ wcel 2136  (class class class)co 5841  ℂcc 7747   + caddc 7752

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

This theorem is referenced by:  muladd11r  8050  comraddd  8051  subadd2  8098  pncan  8100  npcan  8103  subcan  8149  mvlladdd  8259  subaddeqd  8263  addrsub  8265  ltadd1  8323  leadd2  8325  ltsubadd2  8327  lesubadd2  8329  mulreim  8498  apadd2  8503  recp1lt1  8790  ltaddrp2d  9663  lincmb01cmp  9935  iccf1o  9936  rebtwn2zlemstep  10184  qavgle  10190  modqaddabs  10293  mulqaddmodid  10295  qnegmod  10300  modqadd2mod  10305  modqadd12d  10311  modqaddmulmod  10322  addmodlteq  10329  expaddzap  10495  bcn2m1  10678  bcn2p1  10679  remullem  10809  resqrexlemover  10948  maxabslemab  11144  maxabslemval  11146  bdtrilem  11176  climaddc2  11267  telfsumo  11403  fsumparts  11407  bcxmas  11426  isumshft  11427  cvgratnnlemsumlt  11465  cosneg  11664  sinadd  11673  sincossq  11685  cos2t  11687  absefi  11705  absefib  11707  gcdaddm  11913  pythagtrip  12211  metrtri  12977  2sqlem3  13553  apdifflemf  13885  apdiff  13887