Theorem addcomd 8420

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2203  (class class class)co 6049  ℂcc 8121   + caddc 8126

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

This theorem is referenced by:  muladd11r  8425  comraddd  8426  subadd2  8473  pncan  8475  npcan  8478  subcan  8524  mvlladdd  8634  subaddeqd  8638  addrsub  8640  ltadd1  8699  leadd2  8701  ltsubadd2  8703  lesubadd2  8705  mulreim  8874  apadd2  8879  recp1lt1  9169  ltaddrp2d  10060  lincmb01cmp  10332  iccf1o  10334  elfzoext  10533  rebtwn2zlemstep  10608  qavgle  10614  modqaddabs  10720  mulqaddmodid  10722  qnegmod  10727  modqadd2mod  10732  modqadd12d  10738  modqaddmulmod  10749  addmodlteq  10756  expaddzap  10941  bcn2m1  11127  bcn2p1  11128  lenrevpfxcctswrd  11397  remullem  11549  resqrexlemover  11688  maxabslemab  11884  maxabslemval  11886  bdtrilem  11917  climaddc2  12008  telfsumo  12145  fsumparts  12149  bcxmas  12168  isumshft  12169  cvgratnnlemsumlt  12207  cosneg  12406  sinadd  12415  sincossq  12427  cos2t  12429  absefi  12448  absefib  12450  gcdaddm  12673  pythagtrip  12974  pcadd2  13032  mulgnndir  13857  mulgdirlem  13859  metrtri  15229  plymullem1  15600  pellexlem2  15833  lgseisenlem1  15930  2sqlem3  15977  eupth2lem3lem3fi  16452  apdifflemf  16817  apdiff  16819