Theorem addcomd 8108

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

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148  (class class class)co 5875  ℂcc 7809   + caddc 7814

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

This theorem is referenced by:  muladd11r  8113  comraddd  8114  subadd2  8161  pncan  8163  npcan  8166  subcan  8212  mvlladdd  8322  subaddeqd  8326  addrsub  8328  ltadd1  8386  leadd2  8388  ltsubadd2  8390  lesubadd2  8392  mulreim  8561  apadd2  8566  recp1lt1  8856  ltaddrp2d  9731  lincmb01cmp  10003  iccf1o  10004  rebtwn2zlemstep  10253  qavgle  10259  modqaddabs  10362  mulqaddmodid  10364  qnegmod  10369  modqadd2mod  10374  modqadd12d  10380  modqaddmulmod  10391  addmodlteq  10398  expaddzap  10564  bcn2m1  10749  bcn2p1  10750  remullem  10880  resqrexlemover  11019  maxabslemab  11215  maxabslemval  11217  bdtrilem  11247  climaddc2  11338  telfsumo  11474  fsumparts  11478  bcxmas  11497  isumshft  11498  cvgratnnlemsumlt  11536  cosneg  11735  sinadd  11744  sincossq  11756  cos2t  11758  absefi  11776  absefib  11778  gcdaddm  11985  pythagtrip  12283  mulgnndir  13012  mulgdirlem  13014  metrtri  13880  lgseisenlem1  14453  2sqlem3  14467  apdifflemf  14797  apdiff  14799