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

Theorem addcomli 7900
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 7899 . 2 (𝐵 + 𝐴) = (𝐴 + 𝐵)
4 addcomli.2 . 2 (𝐴 + 𝐵) = 𝐶
53, 4eqtri 2158 1 (𝐵 + 𝐴) = 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1331  wcel 1480  (class class class)co 5767  cc 7611   + caddc 7616
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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119  ax-addcom 7713
This theorem depends on definitions:  df-bi 116  df-cleq 2130
This theorem is referenced by:  negsubdi2i  8041  1p2e3  8847  peano2z  9083  4t4e16  9273  6t3e18  9279  6t5e30  9281  7t3e21  9284  7t4e28  9285  7t6e42  9287  7t7e49  9288  8t3e24  9290  8t4e32  9291  8t5e40  9292  8t8e64  9295  9t3e27  9297  9t4e36  9298  9t5e45  9299  9t6e54  9300  9t7e63  9301  9t8e72  9302  9t9e81  9303  4bc3eq4  10512  n2dvdsm1  11599  6gcd4e2  11672  eulerid  12872  cosq23lt0  12903  ex-exp  12928  ex-bc  12930  ex-gcd  12932
  Copyright terms: Public domain W3C validator