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

Theorem addcomd 7906
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 7892 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  =  ( B  +  A ) )
41, 2, 3syl2anc 408 1  |-  ( ph  ->  ( A  +  B
)  =  ( B  +  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1331    e. wcel 1480  (class class class)co 5767   CCcc 7611    + caddc 7616
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-addcom 7713
This theorem is referenced by:  muladd11r  7911  comraddd  7912  subadd2  7959  pncan  7961  npcan  7964  subcan  8010  mvlladdd  8120  subaddeqd  8124  addrsub  8126  ltadd1  8184  leadd2  8186  ltsubadd2  8188  lesubadd2  8190  mulreim  8359  apadd2  8364  recp1lt1  8650  ltaddrp2d  9511  lincmb01cmp  9779  iccf1o  9780  rebtwn2zlemstep  10023  qavgle  10029  modqaddabs  10128  mulqaddmodid  10130  qnegmod  10135  modqadd2mod  10140  modqadd12d  10146  modqaddmulmod  10157  addmodlteq  10164  expaddzap  10330  bcn2m1  10508  bcn2p1  10509  remullem  10636  resqrexlemover  10775  maxabslemab  10971  maxabslemval  10973  bdtrilem  11003  climaddc2  11092  telfsumo  11228  fsumparts  11232  bcxmas  11251  isumshft  11252  cvgratnnlemsumlt  11290  cosneg  11423  sinadd  11432  sincossq  11444  cos2t  11446  absefi  11464  absefib  11466  gcdaddm  11661  metrtri  12535
  Copyright terms: Public domain W3C validator