Theorem addcomd 7694

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

Syntax hints:   → wi 4   = wceq 1290   ∈ wcel 1439  (class class class)co 5666  ℂcc 7409   + caddc 7414

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

This theorem is referenced by:  muladd11r  7699  comraddd  7700  subadd2  7747  pncan  7749  npcan  7752  subcan  7798  subaddeqd  7908  addrsub  7910  ltadd1  7968  leadd2  7970  ltsubadd2  7972  lesubadd2  7974  mulreim  8142  apadd2  8147  recp1lt1  8421  ltaddrp2d  9269  lincmb01cmp  9481  iccf1o  9482  rebtwn2zlemstep  9725  qavgle  9731  modqaddabs  9830  mulqaddmodid  9832  qnegmod  9837  modqadd2mod  9842  modqadd12d  9848  modqaddmulmod  9859  addmodlteq  9866  expaddzap  10060  bcn2m1  10238  bcn2p1  10239  remullem  10366  resqrexlemover  10504  maxabslemab  10700  maxabslemval  10702  climaddc2  10779  telfsumo  10921  fsumparts  10925  bcxmas  10944  isumshft  10945  cvgratnnlemsumlt  10983  cosneg  11079  sinadd  11088  sincossq  11100  cos2t  11102  absefi  11119  absefib  11121  gcdaddm  11314