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

Theorem addcomli 8020
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 8019 . 2 (𝐵 + 𝐴) = (𝐴 + 𝐵)
4 addcomli.2 . 2 (𝐴 + 𝐵) = 𝐶
53, 4eqtri 2178 1 (𝐵 + 𝐴) = 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1335  wcel 2128  (class class class)co 5824  cc 7730   + caddc 7735
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ext 2139  ax-addcom 7832
This theorem depends on definitions:  df-bi 116  df-cleq 2150
This theorem is referenced by:  negsubdi2i  8161  1p2e3  8967  peano2z  9203  4t4e16  9393  6t3e18  9399  6t5e30  9401  7t3e21  9404  7t4e28  9405  7t6e42  9407  7t7e49  9408  8t3e24  9410  8t4e32  9411  8t5e40  9412  8t8e64  9415  9t3e27  9417  9t4e36  9418  9t5e45  9419  9t6e54  9420  9t7e63  9421  9t8e72  9422  9t9e81  9423  4bc3eq4  10647  n2dvdsm1  11804  6gcd4e2  11879  eulerid  13134  cosq23lt0  13165  binom4  13307  ex-exp  13314  ex-bc  13316  ex-gcd  13318
  Copyright terms: Public domain W3C validator