Theorem addcomd 8485

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 8471	. 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 8184   + caddc 8189

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

This theorem is used by:  muladd11r  8490  comraddd  8491  subadd2  8538  pncan  8540  npcan  8543  subcan  8589  mvlladdd  8699  subaddeqd  8703  addrsub  8705  ltadd1  8765  leadd2  8767  ltsubadd2  8769  lesubadd2  8771  lesub3d  8899  mulreim  8941  apadd2  8946  recp1lt1  9238  ltaddrp2d  10150  lincmb01cmp  10423  iccf1o  10425  elfzoext  10628  rebtwn2zlemstep  10705  qavgle  10711  modqaddabs  10821  mulqaddmodid  10823  qnegmod  10828  modqadd2mod  10833  modqadd12d  10839  modqaddmulmod  10850  addmodlteq  10857  expaddzap  11042  bcn2m1  11231  bcn2p1  11232  lenrevpfxcctswrd  11507  remullem  11659  resqrexlemover  11799  maxabslemab  11996  maxabslemval  11998  bdtrilem  12031  climaddc2  12122  telfsumo  12259  fsumparts  12263  bcxmas  12282  isumshft  12283  cvgratnnlemsumlt  12321  cosneg  12520  sinadd  12529  sincossq  12541  cos2t  12543  absefi  12562  absefib  12564  gcdaddm  12787  pythagtrip  13092  pcadd2  13150  ballotfilemsdom  13314  mulgnndir  14014  mulgdirlem  14016  metrtri  15615  plymullem1  15986  efap1p  16017  pellexlem2  16242  bposlem9  16331  lgseisenlem1  16406  2sqlem3  16453  eupth2lem3lem3fi  16928  apdifflemf  17314  apdiff  17316