Theorem addcomd 8313

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  (class class class)co 6010  ℂcc 8013   + caddc 8018

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

This theorem is referenced by:  muladd11r  8318  comraddd  8319  subadd2  8366  pncan  8368  npcan  8371  subcan  8417  mvlladdd  8527  subaddeqd  8531  addrsub  8533  ltadd1  8592  leadd2  8594  ltsubadd2  8596  lesubadd2  8598  mulreim  8767  apadd2  8772  recp1lt1  9062  ltaddrp2d  9944  lincmb01cmp  10216  iccf1o  10217  elfzoext  10415  rebtwn2zlemstep  10489  qavgle  10495  modqaddabs  10601  mulqaddmodid  10603  qnegmod  10608  modqadd2mod  10613  modqadd12d  10619  modqaddmulmod  10630  addmodlteq  10637  expaddzap  10822  bcn2m1  11008  bcn2p1  11009  lenrevpfxcctswrd  11265  remullem  11403  resqrexlemover  11542  maxabslemab  11738  maxabslemval  11740  bdtrilem  11771  climaddc2  11862  telfsumo  11998  fsumparts  12002  bcxmas  12021  isumshft  12022  cvgratnnlemsumlt  12060  cosneg  12259  sinadd  12268  sincossq  12280  cos2t  12282  absefi  12301  absefib  12303  gcdaddm  12526  pythagtrip  12827  pcadd2  12885  mulgnndir  13709  mulgdirlem  13711  metrtri  15072  plymullem1  15443  lgseisenlem1  15770  2sqlem3  15817  apdifflemf  16528  apdiff  16530