Theorem addcomd 8230

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2177  (class class class)co 5951  ℂcc 7930   + caddc 7935

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

This theorem is referenced by:  muladd11r  8235  comraddd  8236  subadd2  8283  pncan  8285  npcan  8288  subcan  8334  mvlladdd  8444  subaddeqd  8448  addrsub  8450  ltadd1  8509  leadd2  8511  ltsubadd2  8513  lesubadd2  8515  mulreim  8684  apadd2  8689  recp1lt1  8979  ltaddrp2d  9860  lincmb01cmp  10132  iccf1o  10133  elfzoext  10328  rebtwn2zlemstep  10402  qavgle  10408  modqaddabs  10514  mulqaddmodid  10516  qnegmod  10521  modqadd2mod  10526  modqadd12d  10532  modqaddmulmod  10543  addmodlteq  10550  expaddzap  10735  bcn2m1  10921  bcn2p1  10922  remullem  11226  resqrexlemover  11365  maxabslemab  11561  maxabslemval  11563  bdtrilem  11594  climaddc2  11685  telfsumo  11821  fsumparts  11825  bcxmas  11844  isumshft  11845  cvgratnnlemsumlt  11883  cosneg  12082  sinadd  12091  sincossq  12103  cos2t  12105  absefi  12124  absefib  12126  gcdaddm  12349  pythagtrip  12650  pcadd2  12708  mulgnndir  13531  mulgdirlem  13533  metrtri  14893  plymullem1  15264  lgseisenlem1  15591  2sqlem3  15638  apdifflemf  16059  apdiff  16061