Theorem addcomd 7937

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

Syntax hints:   → wi 4   = wceq 1332   ∈ wcel 1481  (class class class)co 5782  ℂcc 7642   + caddc 7647

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

This theorem is referenced by:  muladd11r  7942  comraddd  7943  subadd2  7990  pncan  7992  npcan  7995  subcan  8041  mvlladdd  8151  subaddeqd  8155  addrsub  8157  ltadd1  8215  leadd2  8217  ltsubadd2  8219  lesubadd2  8221  mulreim  8390  apadd2  8395  recp1lt1  8681  ltaddrp2d  9548  lincmb01cmp  9816  iccf1o  9817  rebtwn2zlemstep  10061  qavgle  10067  modqaddabs  10166  mulqaddmodid  10168  qnegmod  10173  modqadd2mod  10178  modqadd12d  10184  modqaddmulmod  10195  addmodlteq  10202  expaddzap  10368  bcn2m1  10547  bcn2p1  10548  remullem  10675  resqrexlemover  10814  maxabslemab  11010  maxabslemval  11012  bdtrilem  11042  climaddc2  11131  telfsumo  11267  fsumparts  11271  bcxmas  11290  isumshft  11291  cvgratnnlemsumlt  11329  cosneg  11470  sinadd  11479  sincossq  11491  cos2t  11493  absefi  11511  absefib  11513  gcdaddm  11708  metrtri  12585  apdifflemf  13414  apdiff  13416