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

Theorem addcomli 7606
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 7605 . 2  |-  ( B  +  A )  =  ( A  +  B
)
4 addcomli.2 . 2  |-  ( A  +  B )  =  C
53, 4eqtri 2108 1  |-  ( B  +  A )  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1289    e. wcel 1438  (class class class)co 5634   CCcc 7327    + caddc 7332
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-4 1445  ax-17 1464  ax-ext 2070  ax-addcom 7424
This theorem depends on definitions:  df-bi 115  df-cleq 2081
This theorem is referenced by:  negsubdi2i  7747  1p2e3  8520  peano2z  8756  4t4e16  8944  6t3e18  8950  6t5e30  8952  7t3e21  8955  7t4e28  8956  7t6e42  8958  7t7e49  8959  8t3e24  8961  8t4e32  8962  8t5e40  8963  8t8e64  8966  9t3e27  8968  9t4e36  8969  9t5e45  8970  9t6e54  8971  9t7e63  8972  9t8e72  8973  9t9e81  8974  4bc3eq4  10146  n2dvdsm1  10995  6gcd4e2  11066  ex-exp  11300  ex-bc  11302  ex-gcd  11304
  Copyright terms: Public domain W3C validator