Theorem addcomd 8478

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 8464	. 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  8483  comraddd  8484  subadd2  8531  pncan  8533  npcan  8536  subcan  8582  mvlladdd  8692  subaddeqd  8696  addrsub  8698  ltadd1  8758  leadd2  8760  ltsubadd2  8762  lesubadd2  8764  lesub3d  8892  mulreim  8934  apadd2  8939  recp1lt1  9231  ltaddrp2d  10142  lincmb01cmp  10415  iccf1o  10417  elfzoext  10620  rebtwn2zlemstep  10697  qavgle  10703  modqaddabs  10812  mulqaddmodid  10814  qnegmod  10819  modqadd2mod  10824  modqadd12d  10830  modqaddmulmod  10841  addmodlteq  10848  expaddzap  11033  bcn2m1  11222  bcn2p1  11223  lenrevpfxcctswrd  11498  remullem  11650  resqrexlemover  11790  maxabslemab  11987  maxabslemval  11989  bdtrilem  12021  climaddc2  12112  telfsumo  12249  fsumparts  12253  bcxmas  12272  isumshft  12273  cvgratnnlemsumlt  12311  cosneg  12510  sinadd  12519  sincossq  12531  cos2t  12533  absefi  12552  absefib  12554  gcdaddm  12777  pythagtrip  13082  pcadd2  13140  ballotfilemsdom  13304  mulgnndir  14003  mulgdirlem  14005  metrtri  15527  plymullem1  15898  efap1p  15929  pellexlem2  16149  lgseisenlem1  16308  2sqlem3  16355  eupth2lem3lem3fi  16830  apdifflemf  17214  apdiff  17216