Theorem addcomd 8070

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

Syntax hints:   → wi 4   = wceq 1348   ∈ wcel 2141  (class class class)co 5853  ℂcc 7772   + caddc 7777

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

This theorem is referenced by:  muladd11r  8075  comraddd  8076  subadd2  8123  pncan  8125  npcan  8128  subcan  8174  mvlladdd  8284  subaddeqd  8288  addrsub  8290  ltadd1  8348  leadd2  8350  ltsubadd2  8352  lesubadd2  8354  mulreim  8523  apadd2  8528  recp1lt1  8815  ltaddrp2d  9688  lincmb01cmp  9960  iccf1o  9961  rebtwn2zlemstep  10209  qavgle  10215  modqaddabs  10318  mulqaddmodid  10320  qnegmod  10325  modqadd2mod  10330  modqadd12d  10336  modqaddmulmod  10347  addmodlteq  10354  expaddzap  10520  bcn2m1  10703  bcn2p1  10704  remullem  10835  resqrexlemover  10974  maxabslemab  11170  maxabslemval  11172  bdtrilem  11202  climaddc2  11293  telfsumo  11429  fsumparts  11433  bcxmas  11452  isumshft  11453  cvgratnnlemsumlt  11491  cosneg  11690  sinadd  11699  sincossq  11711  cos2t  11713  absefi  11731  absefib  11733  gcdaddm  11939  pythagtrip  12237  metrtri  13171  2sqlem3  13747  apdifflemf  14078  apdiff  14080