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

Theorem addcomd 8041
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  |-  ( ph  ->  A  e.  CC )
addcomd.2  |-  ( ph  ->  B  e.  CC )
Assertion
Ref Expression
addcomd  |-  ( ph  ->  ( A  +  B
)  =  ( B  +  A ) )

Proof of Theorem addcomd
StepHypRef Expression
1 muld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addcomd.2 . 2  |-  ( ph  ->  B  e.  CC )
3 addcom 8027 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  =  ( B  +  A ) )
41, 2, 3syl2anc 409 1  |-  ( ph  ->  ( A  +  B
)  =  ( B  +  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1342    e. wcel 2135  (class class class)co 5837   CCcc 7743    + caddc 7748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-addcom 7845
This theorem is referenced by:  muladd11r  8046  comraddd  8047  subadd2  8094  pncan  8096  npcan  8099  subcan  8145  mvlladdd  8255  subaddeqd  8259  addrsub  8261  ltadd1  8319  leadd2  8321  ltsubadd2  8323  lesubadd2  8325  mulreim  8494  apadd2  8499  recp1lt1  8786  ltaddrp2d  9659  lincmb01cmp  9931  iccf1o  9932  rebtwn2zlemstep  10179  qavgle  10185  modqaddabs  10288  mulqaddmodid  10290  qnegmod  10295  modqadd2mod  10300  modqadd12d  10306  modqaddmulmod  10317  addmodlteq  10324  expaddzap  10490  bcn2m1  10672  bcn2p1  10673  remullem  10800  resqrexlemover  10939  maxabslemab  11135  maxabslemval  11137  bdtrilem  11167  climaddc2  11258  telfsumo  11394  fsumparts  11398  bcxmas  11417  isumshft  11418  cvgratnnlemsumlt  11456  cosneg  11655  sinadd  11664  sincossq  11676  cos2t  11678  absefi  11696  absefib  11698  gcdaddm  11903  pythagtrip  12201  metrtri  12935  apdifflemf  13777  apdiff  13779
  Copyright terms: Public domain W3C validator