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

Theorem addcomd 7623
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 7609 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  =  ( B  +  A ) )
41, 2, 3syl2anc 403 1  |-  ( ph  ->  ( A  +  B
)  =  ( B  +  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1289    e. wcel 1438  (class class class)co 5644   CCcc 7338    + caddc 7343
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106  ax-addcom 7435
This theorem is referenced by:  muladd11r  7628  comraddd  7629  subadd2  7676  pncan  7678  npcan  7681  subcan  7727  subaddeqd  7837  addrsub  7839  ltadd1  7897  leadd2  7899  ltsubadd2  7901  lesubadd2  7903  mulreim  8071  apadd2  8076  recp1lt1  8350  ltaddrp2d  9198  lincmb01cmp  9410  iccf1o  9411  rebtwn2zlemstep  9652  qavgle  9658  modqaddabs  9757  mulqaddmodid  9759  qnegmod  9764  modqadd2mod  9769  modqadd12d  9775  modqaddmulmod  9786  addmodlteq  9793  expaddzap  9987  bcn2m1  10165  bcn2p1  10166  remullem  10293  resqrexlemover  10431  maxabslemab  10627  maxabslemval  10629  climaddc2  10705  telfsumo  10847  fsumparts  10851  bcxmas  10870  isumshft  10871  cvgratnnlemsumlt  10909  cosneg  11005  sinadd  11014  sincossq  11026  cos2t  11028  absefi  11045  absefib  11047  gcdaddm  11240
  Copyright terms: Public domain W3C validator