Theorem addcomd 8305

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  (class class class)co 6007  ℂcc 8005   + caddc 8010

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

This theorem is referenced by:  muladd11r  8310  comraddd  8311  subadd2  8358  pncan  8360  npcan  8363  subcan  8409  mvlladdd  8519  subaddeqd  8523  addrsub  8525  ltadd1  8584  leadd2  8586  ltsubadd2  8588  lesubadd2  8590  mulreim  8759  apadd2  8764  recp1lt1  9054  ltaddrp2d  9935  lincmb01cmp  10207  iccf1o  10208  elfzoext  10406  rebtwn2zlemstep  10480  qavgle  10486  modqaddabs  10592  mulqaddmodid  10594  qnegmod  10599  modqadd2mod  10604  modqadd12d  10610  modqaddmulmod  10621  addmodlteq  10628  expaddzap  10813  bcn2m1  10999  bcn2p1  11000  lenrevpfxcctswrd  11252  remullem  11390  resqrexlemover  11529  maxabslemab  11725  maxabslemval  11727  bdtrilem  11758  climaddc2  11849  telfsumo  11985  fsumparts  11989  bcxmas  12008  isumshft  12009  cvgratnnlemsumlt  12047  cosneg  12246  sinadd  12255  sincossq  12267  cos2t  12269  absefi  12288  absefib  12290  gcdaddm  12513  pythagtrip  12814  pcadd2  12872  mulgnndir  13696  mulgdirlem  13698  metrtri  15059  plymullem1  15430  lgseisenlem1  15757  2sqlem3  15804  apdifflemf  16444  apdiff  16446