Theorem addcomd 8265

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

Syntax hints:   → wi 4   = wceq 1375   ∈ wcel 2180  (class class class)co 5974  ℂcc 7965   + caddc 7970

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

This theorem is referenced by:  muladd11r  8270  comraddd  8271  subadd2  8318  pncan  8320  npcan  8323  subcan  8369  mvlladdd  8479  subaddeqd  8483  addrsub  8485  ltadd1  8544  leadd2  8546  ltsubadd2  8548  lesubadd2  8550  mulreim  8719  apadd2  8724  recp1lt1  9014  ltaddrp2d  9895  lincmb01cmp  10167  iccf1o  10168  elfzoext  10365  rebtwn2zlemstep  10439  qavgle  10445  modqaddabs  10551  mulqaddmodid  10553  qnegmod  10558  modqadd2mod  10563  modqadd12d  10569  modqaddmulmod  10580  addmodlteq  10587  expaddzap  10772  bcn2m1  10958  bcn2p1  10959  lenrevpfxcctswrd  11210  remullem  11348  resqrexlemover  11487  maxabslemab  11683  maxabslemval  11685  bdtrilem  11716  climaddc2  11807  telfsumo  11943  fsumparts  11947  bcxmas  11966  isumshft  11967  cvgratnnlemsumlt  12005  cosneg  12204  sinadd  12213  sincossq  12225  cos2t  12227  absefi  12246  absefib  12248  gcdaddm  12471  pythagtrip  12772  pcadd2  12830  mulgnndir  13654  mulgdirlem  13656  metrtri  15016  plymullem1  15387  lgseisenlem1  15714  2sqlem3  15761  apdifflemf  16325  apdiff  16327