Theorem addcomd 8172

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2164  (class class class)co 5919  ℂcc 7872   + caddc 7877

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

This theorem is referenced by:  muladd11r  8177  comraddd  8178  subadd2  8225  pncan  8227  npcan  8230  subcan  8276  mvlladdd  8386  subaddeqd  8390  addrsub  8392  ltadd1  8450  leadd2  8452  ltsubadd2  8454  lesubadd2  8456  mulreim  8625  apadd2  8630  recp1lt1  8920  ltaddrp2d  9800  lincmb01cmp  10072  iccf1o  10073  rebtwn2zlemstep  10324  qavgle  10330  modqaddabs  10436  mulqaddmodid  10438  qnegmod  10443  modqadd2mod  10448  modqadd12d  10454  modqaddmulmod  10465  addmodlteq  10472  expaddzap  10657  bcn2m1  10843  bcn2p1  10844  remullem  11018  resqrexlemover  11157  maxabslemab  11353  maxabslemval  11355  bdtrilem  11385  climaddc2  11476  telfsumo  11612  fsumparts  11616  bcxmas  11635  isumshft  11636  cvgratnnlemsumlt  11674  cosneg  11873  sinadd  11882  sincossq  11894  cos2t  11896  absefi  11915  absefib  11917  gcdaddm  12124  pythagtrip  12424  pcadd2  12482  mulgnndir  13224  mulgdirlem  13226  metrtri  14556  plymullem1  14927  lgseisenlem1  15227  2sqlem3  15274  apdifflemf  15606  apdiff  15608