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 8019 | . 2 ⊢ (𝐵 + 𝐴) = (𝐴 + 𝐵) |
4 | addcomli.2 | . 2 ⊢ (𝐴 + 𝐵) = 𝐶 | |
5 | 3, 4 | eqtri 2178 | 1 ⊢ (𝐵 + 𝐴) = 𝐶 |
Colors of variables: wff set class |
Syntax hints: = wceq 1335 ∈ wcel 2128 (class class class)co 5824 ℂcc 7730 + caddc 7735 |
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 1427 ax-gen 1429 ax-4 1490 ax-17 1506 ax-ext 2139 ax-addcom 7832 |
This theorem depends on definitions: df-bi 116 df-cleq 2150 |
This theorem is referenced by: negsubdi2i 8161 1p2e3 8967 peano2z 9203 4t4e16 9393 6t3e18 9399 6t5e30 9401 7t3e21 9404 7t4e28 9405 7t6e42 9407 7t7e49 9408 8t3e24 9410 8t4e32 9411 8t5e40 9412 8t8e64 9415 9t3e27 9417 9t4e36 9418 9t5e45 9419 9t6e54 9420 9t7e63 9421 9t8e72 9422 9t9e81 9423 4bc3eq4 10647 n2dvdsm1 11804 6gcd4e2 11879 eulerid 13134 cosq23lt0 13165 binom4 13307 ex-exp 13314 ex-bc 13316 ex-gcd 13318 |
Copyright terms: Public domain | W3C validator |