Theorem addcomd 8128

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2160  (class class class)co 5892  ℂcc 7829   + caddc 7834

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

This theorem is referenced by:  muladd11r  8133  comraddd  8134  subadd2  8181  pncan  8183  npcan  8186  subcan  8232  mvlladdd  8342  subaddeqd  8346  addrsub  8348  ltadd1  8406  leadd2  8408  ltsubadd2  8410  lesubadd2  8412  mulreim  8581  apadd2  8586  recp1lt1  8876  ltaddrp2d  9751  lincmb01cmp  10023  iccf1o  10024  rebtwn2zlemstep  10273  qavgle  10279  modqaddabs  10382  mulqaddmodid  10384  qnegmod  10389  modqadd2mod  10394  modqadd12d  10400  modqaddmulmod  10411  addmodlteq  10418  expaddzap  10584  bcn2m1  10769  bcn2p1  10770  remullem  10900  resqrexlemover  11039  maxabslemab  11235  maxabslemval  11237  bdtrilem  11267  climaddc2  11358  telfsumo  11494  fsumparts  11498  bcxmas  11517  isumshft  11518  cvgratnnlemsumlt  11556  cosneg  11755  sinadd  11764  sincossq  11776  cos2t  11778  absefi  11796  absefib  11798  gcdaddm  12005  pythagtrip  12303  mulgnndir  13064  mulgdirlem  13066  metrtri  14289  lgseisenlem1  14862  2sqlem3  14876  apdifflemf  15207  apdiff  15209