Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > addcomli | GIF version |
Description: Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015.) |
Ref | Expression |
---|---|
mul.1 | ⊢ 𝐴 ∈ ℂ |
mul.2 | ⊢ 𝐵 ∈ ℂ |
addcomli.2 | ⊢ (𝐴 + 𝐵) = 𝐶 |
Ref | Expression |
---|---|
addcomli | ⊢ (𝐵 + 𝐴) = 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mul.2 | . . 3 ⊢ 𝐵 ∈ ℂ | |
2 | mul.1 | . . 3 ⊢ 𝐴 ∈ ℂ | |
3 | 1, 2 | addcomi 8063 | . 2 ⊢ (𝐵 + 𝐴) = (𝐴 + 𝐵) |
4 | addcomli.2 | . 2 ⊢ (𝐴 + 𝐵) = 𝐶 | |
5 | 3, 4 | eqtri 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 |