Theorem addcomd 7259

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

Syntax hints:   → wi 4   = wceq 1284   ∈ wcel 1433  (class class class)co 5532  ℂcc 6979   + caddc 6984

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

This theorem is referenced by:  muladd11r  7264  comraddd  7265  subadd2  7312  pncan  7314  npcan  7317  subcan  7363  subaddeqd  7473  addrsub  7475  ltadd1  7533  leadd2  7535  ltsubadd2  7537  lesubadd2  7539  mulreim  7704  apadd2  7709  recp1lt1  7977  ltaddrp2d  8808  lincmb01cmp  9025  iccf1o  9026  rebtwn2zlemstep  9261  qavgle  9267  modqaddabs  9364  mulqaddmodid  9366  qnegmod  9371  modqadd2mod  9376  modqadd12d  9382  modqaddmulmod  9393  addmodlteq  9400  expaddzap  9520  bcn2m1  9696  bcn2p1  9697  remullem  9758  resqrexlemover  9896  maxabslemab  10092  maxabslemval  10094  climaddc2  10168  clim2iser2  10176  gcdaddm  10375