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

Theorem addcomli 7309
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 7308 . 2  |-  ( B  +  A )  =  ( A  +  B
)
4 addcomli.2 . 2  |-  ( A  +  B )  =  C
53, 4eqtri 2102 1  |-  ( B  +  A )  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1285    e. wcel 1434  (class class class)co 5537   CCcc 7030    + caddc 7035
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 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064  ax-addcom 7127
This theorem depends on definitions:  df-bi 115  df-cleq 2075
This theorem is referenced by:  negsubdi2i  7450  1p2e3  8222  peano2z  8457  4t4e16  8645  6t3e18  8651  6t5e30  8653  7t3e21  8656  7t4e28  8657  7t6e42  8659  7t7e49  8660  8t3e24  8662  8t4e32  8663  8t5e40  8664  8t8e64  8667  9t3e27  8669  9t4e36  8670  9t5e45  8671  9t6e54  8672  9t7e63  8673  9t8e72  8674  9t9e81  8675  4bc3eq4  9786  n2dvdsm1  10446  6gcd4e2  10517  ex-bc  10702  ex-gcd  10704
  Copyright terms: Public domain W3C validator