Theorem addcomd 8330

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

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2202  (class class class)co 6018  ℂcc 8030   + caddc 8035

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

This theorem is referenced by:  muladd11r  8335  comraddd  8336  subadd2  8383  pncan  8385  npcan  8388  subcan  8434  mvlladdd  8544  subaddeqd  8548  addrsub  8550  ltadd1  8609  leadd2  8611  ltsubadd2  8613  lesubadd2  8615  mulreim  8784  apadd2  8789  recp1lt1  9079  ltaddrp2d  9966  lincmb01cmp  10238  iccf1o  10239  elfzoext  10438  rebtwn2zlemstep  10513  qavgle  10519  modqaddabs  10625  mulqaddmodid  10627  qnegmod  10632  modqadd2mod  10637  modqadd12d  10643  modqaddmulmod  10654  addmodlteq  10661  expaddzap  10846  bcn2m1  11032  bcn2p1  11033  lenrevpfxcctswrd  11294  remullem  11433  resqrexlemover  11572  maxabslemab  11768  maxabslemval  11770  bdtrilem  11801  climaddc2  11892  telfsumo  12029  fsumparts  12033  bcxmas  12052  isumshft  12053  cvgratnnlemsumlt  12091  cosneg  12290  sinadd  12299  sincossq  12311  cos2t  12313  absefi  12332  absefib  12334  gcdaddm  12557  pythagtrip  12858  pcadd2  12916  mulgnndir  13740  mulgdirlem  13742  metrtri  15104  plymullem1  15475  lgseisenlem1  15802  2sqlem3  15849  eupth2lem3lem3fi  16324  apdifflemf  16671  apdiff  16673