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

Theorem addcomd 8121
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 8107 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
41, 2, 3syl2anc 411 1 (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1363  wcel 2158  (class class class)co 5888  cc 7822   + caddc 7827
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-addcom 7924
This theorem is referenced by:  muladd11r  8126  comraddd  8127  subadd2  8174  pncan  8176  npcan  8179  subcan  8225  mvlladdd  8335  subaddeqd  8339  addrsub  8341  ltadd1  8399  leadd2  8401  ltsubadd2  8403  lesubadd2  8405  mulreim  8574  apadd2  8579  recp1lt1  8869  ltaddrp2d  9744  lincmb01cmp  10016  iccf1o  10017  rebtwn2zlemstep  10266  qavgle  10272  modqaddabs  10375  mulqaddmodid  10377  qnegmod  10382  modqadd2mod  10387  modqadd12d  10393  modqaddmulmod  10404  addmodlteq  10411  expaddzap  10577  bcn2m1  10762  bcn2p1  10763  remullem  10893  resqrexlemover  11032  maxabslemab  11228  maxabslemval  11230  bdtrilem  11260  climaddc2  11351  telfsumo  11487  fsumparts  11491  bcxmas  11510  isumshft  11511  cvgratnnlemsumlt  11549  cosneg  11748  sinadd  11757  sincossq  11769  cos2t  11771  absefi  11789  absefib  11791  gcdaddm  11998  pythagtrip  12296  mulgnndir  13043  mulgdirlem  13045  metrtri  14148  lgseisenlem1  14721  2sqlem3  14735  apdifflemf  15066  apdiff  15068
  Copyright terms: Public domain W3C validator