Theorem addcomd 8182

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167  (class class class)co 5925  ℂcc 7882   + caddc 7887

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

This theorem is referenced by:  muladd11r  8187  comraddd  8188  subadd2  8235  pncan  8237  npcan  8240  subcan  8286  mvlladdd  8396  subaddeqd  8400  addrsub  8402  ltadd1  8461  leadd2  8463  ltsubadd2  8465  lesubadd2  8467  mulreim  8636  apadd2  8641  recp1lt1  8931  ltaddrp2d  9811  lincmb01cmp  10083  iccf1o  10084  rebtwn2zlemstep  10347  qavgle  10353  modqaddabs  10459  mulqaddmodid  10461  qnegmod  10466  modqadd2mod  10471  modqadd12d  10477  modqaddmulmod  10488  addmodlteq  10495  expaddzap  10680  bcn2m1  10866  bcn2p1  10867  remullem  11041  resqrexlemover  11180  maxabslemab  11376  maxabslemval  11378  bdtrilem  11409  climaddc2  11500  telfsumo  11636  fsumparts  11640  bcxmas  11659  isumshft  11660  cvgratnnlemsumlt  11698  cosneg  11897  sinadd  11906  sincossq  11918  cos2t  11920  absefi  11939  absefib  11941  gcdaddm  12164  pythagtrip  12465  pcadd2  12523  mulgnndir  13328  mulgdirlem  13330  metrtri  14660  plymullem1  15031  lgseisenlem1  15358  2sqlem3  15405  apdifflemf  15740  apdiff  15742