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

Theorem addcomli 8105
Description: Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015.)
Hypotheses
Ref Expression
mul.1  |-  A  e.  CC
mul.2  |-  B  e.  CC
addcomli.2  |-  ( A  +  B )  =  C
Assertion
Ref Expression
addcomli  |-  ( B  +  A )  =  C

Proof of Theorem addcomli
StepHypRef Expression
1 mul.2 . . 3  |-  B  e.  CC
2 mul.1 . . 3  |-  A  e.  CC
31, 2addcomi 8104 . 2  |-  ( B  +  A )  =  ( A  +  B
)
4 addcomli.2 . 2  |-  ( A  +  B )  =  C
53, 4eqtri 2198 1  |-  ( B  +  A )  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1353    e. wcel 2148  (class class class)co 5878   CCcc 7812    + caddc 7817
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159  ax-addcom 7914
This theorem depends on definitions:  df-bi 117  df-cleq 2170
This theorem is referenced by:  negsubdi2i  8246  1p2e3  9056  peano2z  9292  4t4e16  9485  6t3e18  9491  6t5e30  9493  7t3e21  9496  7t4e28  9497  7t6e42  9499  7t7e49  9500  8t3e24  9502  8t4e32  9503  8t5e40  9504  8t8e64  9507  9t3e27  9509  9t4e36  9510  9t5e45  9511  9t6e54  9512  9t7e63  9513  9t8e72  9514  9t9e81  9515  4bc3eq4  10756  n2dvdsm1  11921  6gcd4e2  11999  eulerid  14384  cosq23lt0  14415  binom4  14558  lgsdir2lem1  14590  m1lgs  14613  2lgsoddprmlem3d  14619  ex-exp  14640  ex-bc  14642  ex-gcd  14644
  Copyright terms: Public domain W3C validator