Theorem addcomd 8170

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2164  (class class class)co 5918  ℂcc 7870   + caddc 7875

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

This theorem is referenced by:  muladd11r  8175  comraddd  8176  subadd2  8223  pncan  8225  npcan  8228  subcan  8274  mvlladdd  8384  subaddeqd  8388  addrsub  8390  ltadd1  8448  leadd2  8450  ltsubadd2  8452  lesubadd2  8454  mulreim  8623  apadd2  8628  recp1lt1  8918  ltaddrp2d  9797  lincmb01cmp  10069  iccf1o  10070  rebtwn2zlemstep  10321  qavgle  10327  modqaddabs  10433  mulqaddmodid  10435  qnegmod  10440  modqadd2mod  10445  modqadd12d  10451  modqaddmulmod  10462  addmodlteq  10469  expaddzap  10654  bcn2m1  10840  bcn2p1  10841  remullem  11015  resqrexlemover  11154  maxabslemab  11350  maxabslemval  11352  bdtrilem  11382  climaddc2  11473  telfsumo  11609  fsumparts  11613  bcxmas  11632  isumshft  11633  cvgratnnlemsumlt  11671  cosneg  11870  sinadd  11879  sincossq  11891  cos2t  11893  absefi  11912  absefib  11914  gcdaddm  12121  pythagtrip  12421  pcadd2  12479  mulgnndir  13221  mulgdirlem  13223  metrtri  14545  plymullem1  14894  lgseisenlem1  15186  2sqlem3  15204  apdifflemf  15536  apdiff  15538