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

Theorem addcomli 7219
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 7218 . 2 (𝐵 + 𝐴) = (𝐴 + 𝐵)
4 addcomli.2 . 2 (𝐴 + 𝐵) = 𝐶
53, 4eqtri 2076 1 (𝐵 + 𝐴) = 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1259  wcel 1409  (class class class)co 5540  cc 6945   + caddc 6950
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-17 1435  ax-ext 2038  ax-addcom 7042
This theorem depends on definitions:  df-bi 114  df-cleq 2049
This theorem is referenced by:  negsubdi2i  7360  1p2e3  8117  peano2z  8338  4t4e16  8525  6t3e18  8531  6t5e30  8533  7t3e21  8536  7t4e28  8537  7t6e42  8539  7t7e49  8540  8t3e24  8542  8t4e32  8543  8t5e40  8544  8t8e64  8547  9t3e27  8549  9t4e36  8550  9t5e45  8551  9t6e54  8552  9t7e63  8553  9t8e72  8554  9t9e81  8555  4bc3eq4  9641  n2dvdsm1  10225  ex-bc  10282
  Copyright terms: Public domain W3C validator