Theorem addcomd 8471

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

Syntax hints:   → wi 4   = wceq 1402   ∈ wcel 2209  (class class class)co 6079  ℂcc 8171   + caddc 8176

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

This theorem is referenced by:  muladd11r  8476  comraddd  8477  subadd2  8524  pncan  8526  npcan  8529  subcan  8575  mvlladdd  8685  subaddeqd  8689  addrsub  8691  ltadd1  8751  leadd2  8753  ltsubadd2  8755  lesubadd2  8757  mulreim  8926  apadd2  8931  recp1lt1  9223  ltaddrp2d  10115  lincmb01cmp  10388  iccf1o  10390  elfzoext  10593  rebtwn2zlemstep  10670  qavgle  10676  modqaddabs  10782  mulqaddmodid  10784  qnegmod  10789  modqadd2mod  10794  modqadd12d  10800  modqaddmulmod  10811  addmodlteq  10818  expaddzap  11003  bcn2m1  11191  bcn2p1  11192  lenrevpfxcctswrd  11467  remullem  11619  resqrexlemover  11759  maxabslemab  11955  maxabslemval  11957  bdtrilem  11988  climaddc2  12079  telfsumo  12216  fsumparts  12220  bcxmas  12239  isumshft  12240  cvgratnnlemsumlt  12278  cosneg  12477  sinadd  12486  sincossq  12498  cos2t  12500  absefi  12519  absefib  12521  gcdaddm  12744  pythagtrip  13045  pcadd2  13103  ballotfilemsdom  13238  mulgnndir  13937  mulgdirlem  13939  metrtri  15461  plymullem1  15832  pellexlem2  16075  lgseisenlem1  16172  2sqlem3  16219  eupth2lem3lem3fi  16694  apdifflemf  17069  apdiff  17071