Theorem addcomd 8484

Description: Addition is commutative. 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 8470	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
4	1, 2, 3	syl2anc 415	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209  (class class class)co 6088  ℂcc 8183   + caddc 8188

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-addcom 8285

This theorem is used by:  muladd11r  8489  comraddd  8490  subadd2  8537  pncan  8539  npcan  8542  subcan  8588  mvlladdd  8698  subaddeqd  8702  addrsub  8704  ltadd1  8764  leadd2  8766  ltsubadd2  8768  lesubadd2  8770  lesub3d  8898  mulreim  8940  apadd2  8945  recp1lt1  9237  ltaddrp2d  10148  lincmb01cmp  10421  iccf1o  10423  elfzoext  10626  rebtwn2zlemstep  10703  qavgle  10709  modqaddabs  10819  mulqaddmodid  10821  qnegmod  10826  modqadd2mod  10831  modqadd12d  10837  modqaddmulmod  10848  addmodlteq  10855  expaddzap  11040  bcn2m1  11229  bcn2p1  11230  lenrevpfxcctswrd  11505  remullem  11657  resqrexlemover  11797  maxabslemab  11994  maxabslemval  11996  bdtrilem  12029  climaddc2  12120  telfsumo  12257  fsumparts  12261  bcxmas  12280  isumshft  12281  cvgratnnlemsumlt  12319  cosneg  12518  sinadd  12527  sincossq  12539  cos2t  12541  absefi  12560  absefib  12562  gcdaddm  12785  pythagtrip  13090  pcadd2  13148  ballotfilemsdom  13312  mulgnndir  14012  mulgdirlem  14014  metrtri  15620  plymullem1  15991  efap1p  16022  pellexlem2  16247  bposlem9  16336  lgseisenlem1  16411  2sqlem3  16458  eupth2lem3lem3fi  16933  apdifflemf  17319  apdiff  17321