ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  addcomd GIF version

Theorem addcomd 7326
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
StepHypRef Expression
1 muld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addcomd.2 . 2 (𝜑𝐵 ∈ ℂ)
3 addcom 7312 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
41, 2, 3syl2anc 403 1 (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1285  wcel 1434  (class class class)co 5543  cc 7041   + caddc 7046
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106  ax-addcom 7138
This theorem is referenced by:  muladd11r  7331  comraddd  7332  subadd2  7379  pncan  7381  npcan  7384  subcan  7430  subaddeqd  7540  addrsub  7542  ltadd1  7600  leadd2  7602  ltsubadd2  7604  lesubadd2  7606  mulreim  7771  apadd2  7776  recp1lt1  8044  ltaddrp2d  8889  lincmb01cmp  9101  iccf1o  9102  rebtwn2zlemstep  9339  qavgle  9345  modqaddabs  9444  mulqaddmodid  9446  qnegmod  9451  modqadd2mod  9456  modqadd12d  9462  modqaddmulmod  9473  addmodlteq  9480  expaddzap  9617  bcn2m1  9793  bcn2p1  9794  remullem  9896  resqrexlemover  10034  maxabslemab  10230  maxabslemval  10232  climaddc2  10306  clim2iser2  10314  gcdaddm  10519
  Copyright terms: Public domain W3C validator