Theorem addcomd 8479

Description: Addition is commutative. 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 8465	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
4	1, 2, 3	syl2anc 415	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209  (class class class)co 6085  ℂcc 8178   + caddc 8183

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-addcom 8280

This theorem is used by:  muladd11r  8484  comraddd  8485  subadd2  8532  pncan  8534  npcan  8537  subcan  8583  mvlladdd  8693  subaddeqd  8697  addrsub  8699  ltadd1  8759  leadd2  8761  ltsubadd2  8763  lesubadd2  8765  lesub3d  8893  mulreim  8935  apadd2  8940  recp1lt1  9232  ltaddrp2d  10143  lincmb01cmp  10416  iccf1o  10418  elfzoext  10621  rebtwn2zlemstep  10698  qavgle  10704  modqaddabs  10814  mulqaddmodid  10816  qnegmod  10821  modqadd2mod  10826  modqadd12d  10832  modqaddmulmod  10843  addmodlteq  10850  expaddzap  11035  bcn2m1  11224  bcn2p1  11225  lenrevpfxcctswrd  11500  remullem  11652  resqrexlemover  11792  maxabslemab  11989  maxabslemval  11991  bdtrilem  12024  climaddc2  12115  telfsumo  12252  fsumparts  12256  bcxmas  12275  isumshft  12276  cvgratnnlemsumlt  12314  cosneg  12513  sinadd  12522  sincossq  12534  cos2t  12536  absefi  12555  absefib  12557  gcdaddm  12780  pythagtrip  13085  pcadd2  13143  ballotfilemsdom  13307  mulgnndir  14007  mulgdirlem  14009  metrtri  15569  plymullem1  15940  efap1p  15971  pellexlem2  16196  bposlem9  16285  lgseisenlem1  16360  2sqlem3  16407  eupth2lem3lem3fi  16882  apdifflemf  17267  apdiff  17269