Theorem addcomd 8196

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167  (class class class)co 5925  ℂcc 7896   + caddc 7901

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

This theorem is referenced by:  muladd11r  8201  comraddd  8202  subadd2  8249  pncan  8251  npcan  8254  subcan  8300  mvlladdd  8410  subaddeqd  8414  addrsub  8416  ltadd1  8475  leadd2  8477  ltsubadd2  8479  lesubadd2  8481  mulreim  8650  apadd2  8655  recp1lt1  8945  ltaddrp2d  9825  lincmb01cmp  10097  iccf1o  10098  rebtwn2zlemstep  10361  qavgle  10367  modqaddabs  10473  mulqaddmodid  10475  qnegmod  10480  modqadd2mod  10485  modqadd12d  10491  modqaddmulmod  10502  addmodlteq  10509  expaddzap  10694  bcn2m1  10880  bcn2p1  10881  remullem  11055  resqrexlemover  11194  maxabslemab  11390  maxabslemval  11392  bdtrilem  11423  climaddc2  11514  telfsumo  11650  fsumparts  11654  bcxmas  11673  isumshft  11674  cvgratnnlemsumlt  11712  cosneg  11911  sinadd  11920  sincossq  11932  cos2t  11934  absefi  11953  absefib  11955  gcdaddm  12178  pythagtrip  12479  pcadd2  12537  mulgnndir  13359  mulgdirlem  13361  metrtri  14699  plymullem1  15070  lgseisenlem1  15397  2sqlem3  15444  apdifflemf  15781  apdiff  15783