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

Theorem addcom 7211
Description: Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.)
Assertion
Ref Expression
addcom  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  =  ( B  +  A ) )

Proof of Theorem addcom
StepHypRef Expression
1 ax-addcom 7042 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  =  ( B  +  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    = wceq 1259    e. wcel 1409  (class class class)co 5540   CCcc 6945    + caddc 6950
This theorem was proved from axioms:  ax-addcom 7042
This theorem is referenced by:  addid2  7213  readdcan  7214  addcomi  7218  addcomd  7225  add12  7232  add32  7233  add42  7236  cnegexlem1  7249  cnegexlem3  7251  cnegex2  7253  subsub23  7279  pncan2  7281  addsub  7285  addsub12  7287  addsubeq4  7289  sub32  7308  pnpcan2  7314  ppncan  7316  sub4  7319  negsubdi2  7333  ltadd2  7488  ltaddnegr  7494  ltaddsub2  7506  leaddsub2  7508  leltadd  7516  ltaddpos2  7522  addge02  7542  conjmulap  7780  recreclt  7941  avgle1  8222  avgle2  8223  nn0nnaddcl  8270  fzen  9009  fzshftral  9072  flqzadd  9248  addmodidr  9323  nn0ennn  9373  iseradd  9407  bernneq2  9538  shftval2  9655  shftval4  9657  crim  9686  resqrexlemover  9837  climshft2  10058  dvdsaddr  10151  divalgb  10237
  Copyright terms: Public domain W3C validator