Theorem addcomd 8477

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

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

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

This theorem is used by:  muladd11r  8482  comraddd  8483  subadd2  8530  pncan  8532  npcan  8535  subcan  8581  mvlladdd  8691  subaddeqd  8695  addrsub  8697  ltadd1  8757  leadd2  8759  ltsubadd2  8761  lesubadd2  8763  lesub3d  8891  mulreim  8933  apadd2  8938  recp1lt1  9230  ltaddrp2d  10134  lincmb01cmp  10407  iccf1o  10409  elfzoext  10612  rebtwn2zlemstep  10689  qavgle  10695  modqaddabs  10801  mulqaddmodid  10803  qnegmod  10808  modqadd2mod  10813  modqadd12d  10819  modqaddmulmod  10830  addmodlteq  10837  expaddzap  11022  bcn2m1  11210  bcn2p1  11211  lenrevpfxcctswrd  11486  remullem  11638  resqrexlemover  11778  maxabslemab  11974  maxabslemval  11976  bdtrilem  12007  climaddc2  12098  telfsumo  12235  fsumparts  12239  bcxmas  12258  isumshft  12259  cvgratnnlemsumlt  12297  cosneg  12496  sinadd  12505  sincossq  12517  cos2t  12519  absefi  12538  absefib  12540  gcdaddm  12763  pythagtrip  13064  pcadd2  13122  ballotfilemsdom  13257  mulgnndir  13956  mulgdirlem  13958  metrtri  15480  plymullem1  15851  efap1p  15882  pellexlem2  16098  lgseisenlem1  16201  2sqlem3  16248  eupth2lem3lem3fi  16723  apdifflemf  17107  apdiff  17109