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

Theorem addcomli 7827
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 7826 . 2  |-  ( B  +  A )  =  ( A  +  B
)
4 addcomli.2 . 2  |-  ( A  +  B )  =  C
53, 4eqtri 2135 1  |-  ( B  +  A )  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1314    e. wcel 1463  (class class class)co 5728   CCcc 7542    + caddc 7547
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097  ax-addcom 7642
This theorem depends on definitions:  df-bi 116  df-cleq 2108
This theorem is referenced by:  negsubdi2i  7968  1p2e3  8755  peano2z  8991  4t4e16  9181  6t3e18  9187  6t5e30  9189  7t3e21  9192  7t4e28  9193  7t6e42  9195  7t7e49  9196  8t3e24  9198  8t4e32  9199  8t5e40  9200  8t8e64  9203  9t3e27  9205  9t4e36  9206  9t5e45  9207  9t6e54  9208  9t7e63  9209  9t8e72  9210  9t9e81  9211  4bc3eq4  10409  n2dvdsm1  11455  6gcd4e2  11526  ex-exp  12626  ex-bc  12628  ex-gcd  12630
  Copyright terms: Public domain W3C validator