Theorem addcomd 8121

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

Syntax hints:   → wi 4   = wceq 1363   ∈ wcel 2158  (class class class)co 5888  ℂcc 7822   + caddc 7827

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

This theorem is referenced by:  muladd11r  8126  comraddd  8127  subadd2  8174  pncan  8176  npcan  8179  subcan  8225  mvlladdd  8335  subaddeqd  8339  addrsub  8341  ltadd1  8399  leadd2  8401  ltsubadd2  8403  lesubadd2  8405  mulreim  8574  apadd2  8579  recp1lt1  8869  ltaddrp2d  9744  lincmb01cmp  10016  iccf1o  10017  rebtwn2zlemstep  10266  qavgle  10272  modqaddabs  10375  mulqaddmodid  10377  qnegmod  10382  modqadd2mod  10387  modqadd12d  10393  modqaddmulmod  10404  addmodlteq  10411  expaddzap  10577  bcn2m1  10762  bcn2p1  10763  remullem  10893  resqrexlemover  11032  maxabslemab  11228  maxabslemval  11230  bdtrilem  11260  climaddc2  11351  telfsumo  11487  fsumparts  11491  bcxmas  11510  isumshft  11511  cvgratnnlemsumlt  11549  cosneg  11748  sinadd  11757  sincossq  11769  cos2t  11771  absefi  11789  absefib  11791  gcdaddm  11998  pythagtrip  12296  mulgnndir  13043  mulgdirlem  13045  metrtri  14148  lgseisenlem1  14721  2sqlem3  14735  apdifflemf  15066  apdiff  15068