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

Axiom ax-addcom 7041
Description: Addition commutes. Axiom for real and complex numbers, justified by theorem axaddcom 7001. Proofs should normally use addcom 7210 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.)
Assertion
Ref Expression
ax-addcom  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  =  ( B  +  A ) )

Detailed syntax breakdown of Axiom ax-addcom
StepHypRef Expression
1 cA . . . 4  class  A
2 cc 6944 . . . 4  class  CC
31, 2wcel 1409 . . 3  wff  A  e.  CC
4 cB . . . 4  class  B
54, 2wcel 1409 . . 3  wff  B  e.  CC
63, 5wa 101 . 2  wff  ( A  e.  CC  /\  B  e.  CC )
7 caddc 6949 . . . 4  class  +
81, 4, 7co 5539 . . 3  class  ( A  +  B )
94, 1, 7co 5539 . . 3  class  ( B  +  A )
108, 9wceq 1259 . 2  wff  ( A  +  B )  =  ( B  +  A
)
116, 10wi 4 1  wff  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  =  ( B  +  A ) )
Colors of variables: wff set class
This axiom is referenced by:  addcom  7210
  Copyright terms: Public domain W3C validator