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

Theorem addcomli 7617
Description: Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015.)
Hypotheses
Ref Expression
mul.1 𝐴 ∈ ℂ
mul.2 𝐵 ∈ ℂ
addcomli.2 (𝐴 + 𝐵) = 𝐶
Assertion
Ref Expression
addcomli (𝐵 + 𝐴) = 𝐶

Proof of Theorem addcomli
StepHypRef Expression
1 mul.2 . . 3 𝐵 ∈ ℂ
2 mul.1 . . 3 𝐴 ∈ ℂ
31, 2addcomi 7616 . 2 (𝐵 + 𝐴) = (𝐴 + 𝐵)
4 addcomli.2 . 2 (𝐴 + 𝐵) = 𝐶
53, 4eqtri 2108 1 (𝐵 + 𝐴) = 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1289  wcel 1438  (class class class)co 5644  cc 7338   + caddc 7343
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 7435
This theorem depends on definitions:  df-bi 115  df-cleq 2081
This theorem is referenced by:  negsubdi2i  7758  1p2e3  8540  peano2z  8776  4t4e16  8965  6t3e18  8971  6t5e30  8973  7t3e21  8976  7t4e28  8977  7t6e42  8979  7t7e49  8980  8t3e24  8982  8t4e32  8983  8t5e40  8984  8t8e64  8987  9t3e27  8989  9t4e36  8990  9t5e45  8991  9t6e54  8992  9t7e63  8993  9t8e72  8994  9t9e81  8995  4bc3eq4  10169  n2dvdsm1  11178  6gcd4e2  11249  ex-exp  11537  ex-bc  11539  ex-gcd  11541
  Copyright terms: Public domain W3C validator