Theorem addcomd 8441

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2205  (class class class)co 6058  ℂcc 8141   + caddc 8146

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

This theorem is referenced by:  muladd11r  8446  comraddd  8447  subadd2  8494  pncan  8496  npcan  8499  subcan  8545  mvlladdd  8655  subaddeqd  8659  addrsub  8661  ltadd1  8721  leadd2  8723  ltsubadd2  8725  lesubadd2  8727  mulreim  8896  apadd2  8901  recp1lt1  9193  ltaddrp2d  10085  lincmb01cmp  10358  iccf1o  10360  elfzoext  10562  rebtwn2zlemstep  10639  qavgle  10645  modqaddabs  10751  mulqaddmodid  10753  qnegmod  10758  modqadd2mod  10763  modqadd12d  10769  modqaddmulmod  10780  addmodlteq  10787  expaddzap  10972  bcn2m1  11160  bcn2p1  11161  lenrevpfxcctswrd  11432  remullem  11584  resqrexlemover  11723  maxabslemab  11919  maxabslemval  11921  bdtrilem  11952  climaddc2  12043  telfsumo  12180  fsumparts  12184  bcxmas  12203  isumshft  12204  cvgratnnlemsumlt  12242  cosneg  12441  sinadd  12450  sincossq  12462  cos2t  12464  absefi  12483  absefib  12485  gcdaddm  12708  pythagtrip  13009  pcadd2  13067  ballotfilemsdom  13202  mulgnndir  13907  mulgdirlem  13909  metrtri  15371  plymullem1  15742  pellexlem2  15975  lgseisenlem1  16072  2sqlem3  16119  eupth2lem3lem3fi  16594  apdifflemf  16969  apdiff  16971