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

Theorem addcomli 7875
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 7874 . 2 (𝐵 + 𝐴) = (𝐴 + 𝐵)
4 addcomli.2 . 2 (𝐴 + 𝐵) = 𝐶
53, 4eqtri 2138 1 (𝐵 + 𝐴) = 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1316  wcel 1465  (class class class)co 5742  cc 7586   + caddc 7591
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 1408  ax-gen 1410  ax-4 1472  ax-17 1491  ax-ext 2099  ax-addcom 7688
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  negsubdi2i  8016  1p2e3  8822  peano2z  9058  4t4e16  9248  6t3e18  9254  6t5e30  9256  7t3e21  9259  7t4e28  9260  7t6e42  9262  7t7e49  9263  8t3e24  9265  8t4e32  9266  8t5e40  9267  8t8e64  9270  9t3e27  9272  9t4e36  9273  9t5e45  9274  9t6e54  9275  9t7e63  9276  9t8e72  9277  9t9e81  9278  4bc3eq4  10487  n2dvdsm1  11537  6gcd4e2  11610  eulerid  12810  cosq23lt0  12841  ex-exp  12866  ex-bc  12868  ex-gcd  12870
  Copyright terms: Public domain W3C validator