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

Theorem addcomli 8064
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 8063 . 2 (𝐵 + 𝐴) = (𝐴 + 𝐵)
4 addcomli.2 . 2 (𝐴 + 𝐵) = 𝐶
53, 4eqtri 2191 1 (𝐵 + 𝐴) = 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1348  wcel 2141  (class class class)co 5853  cc 7772   + caddc 7777
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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152  ax-addcom 7874
This theorem depends on definitions:  df-bi 116  df-cleq 2163
This theorem is referenced by:  negsubdi2i  8205  1p2e3  9012  peano2z  9248  4t4e16  9441  6t3e18  9447  6t5e30  9449  7t3e21  9452  7t4e28  9453  7t6e42  9455  7t7e49  9456  8t3e24  9458  8t4e32  9459  8t5e40  9460  8t8e64  9463  9t3e27  9465  9t4e36  9466  9t5e45  9467  9t6e54  9468  9t7e63  9469  9t8e72  9470  9t9e81  9471  4bc3eq4  10707  n2dvdsm1  11872  6gcd4e2  11950  eulerid  13517  cosq23lt0  13548  binom4  13691  lgsdir2lem1  13723  ex-exp  13762  ex-bc  13764  ex-gcd  13766
  Copyright terms: Public domain W3C validator