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

Theorem addcomd 7694
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 7680 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
41, 2, 3syl2anc 404 1 (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1290  wcel 1439  (class class class)co 5666  cc 7409   + caddc 7414
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 107  ax-addcom 7506
This theorem is referenced by:  muladd11r  7699  comraddd  7700  subadd2  7747  pncan  7749  npcan  7752  subcan  7798  subaddeqd  7908  addrsub  7910  ltadd1  7968  leadd2  7970  ltsubadd2  7972  lesubadd2  7974  mulreim  8142  apadd2  8147  recp1lt1  8421  ltaddrp2d  9269  lincmb01cmp  9481  iccf1o  9482  rebtwn2zlemstep  9725  qavgle  9731  modqaddabs  9830  mulqaddmodid  9832  qnegmod  9837  modqadd2mod  9842  modqadd12d  9848  modqaddmulmod  9859  addmodlteq  9866  expaddzap  10060  bcn2m1  10238  bcn2p1  10239  remullem  10366  resqrexlemover  10504  maxabslemab  10700  maxabslemval  10702  climaddc2  10779  telfsumo  10921  fsumparts  10925  bcxmas  10944  isumshft  10945  cvgratnnlemsumlt  10983  cosneg  11079  sinadd  11088  sincossq  11100  cos2t  11102  absefi  11119  absefib  11121  gcdaddm  11314
  Copyright terms: Public domain W3C validator