Theorem addcomd 8429

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2205  (class class class)co 6052  ℂcc 8130   + caddc 8135

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

This theorem is referenced by:  muladd11r  8434  comraddd  8435  subadd2  8482  pncan  8484  npcan  8487  subcan  8533  mvlladdd  8643  subaddeqd  8647  addrsub  8649  ltadd1  8708  leadd2  8710  ltsubadd2  8712  lesubadd2  8714  mulreim  8883  apadd2  8888  recp1lt1  9178  ltaddrp2d  10070  lincmb01cmp  10342  iccf1o  10344  elfzoext  10544  rebtwn2zlemstep  10619  qavgle  10625  modqaddabs  10731  mulqaddmodid  10733  qnegmod  10738  modqadd2mod  10743  modqadd12d  10749  modqaddmulmod  10760  addmodlteq  10767  expaddzap  10952  bcn2m1  11140  bcn2p1  11141  lenrevpfxcctswrd  11412  remullem  11564  resqrexlemover  11703  maxabslemab  11899  maxabslemval  11901  bdtrilem  11932  climaddc2  12023  telfsumo  12160  fsumparts  12164  bcxmas  12183  isumshft  12184  cvgratnnlemsumlt  12222  cosneg  12421  sinadd  12430  sincossq  12442  cos2t  12444  absefi  12463  absefib  12465  gcdaddm  12688  pythagtrip  12989  pcadd2  13047  mulgnndir  13889  mulgdirlem  13891  metrtri  15291  plymullem1  15662  pellexlem2  15895  lgseisenlem1  15992  2sqlem3  16039  eupth2lem3lem3fi  16514  apdifflemf  16879  apdiff  16881