![]() |
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 7930 | . 2 ⊢ (𝐵 + 𝐴) = (𝐴 + 𝐵) |
4 | addcomli.2 | . 2 ⊢ (𝐴 + 𝐵) = 𝐶 | |
5 | 3, 4 | eqtri 2161 | 1 ⊢ (𝐵 + 𝐴) = 𝐶 |
Colors of variables: wff set class |
Syntax hints: = wceq 1332 ∈ wcel 1481 (class class class)co 5782 ℂcc 7642 + caddc 7647 |
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 1424 ax-gen 1426 ax-4 1488 ax-17 1507 ax-ext 2122 ax-addcom 7744 |
This theorem depends on definitions: df-bi 116 df-cleq 2133 |
This theorem is referenced by: negsubdi2i 8072 1p2e3 8878 peano2z 9114 4t4e16 9304 6t3e18 9310 6t5e30 9312 7t3e21 9315 7t4e28 9316 7t6e42 9318 7t7e49 9319 8t3e24 9321 8t4e32 9322 8t5e40 9323 8t8e64 9326 9t3e27 9328 9t4e36 9329 9t5e45 9330 9t6e54 9331 9t7e63 9332 9t8e72 9333 9t9e81 9334 4bc3eq4 10551 n2dvdsm1 11646 6gcd4e2 11719 eulerid 12931 cosq23lt0 12962 ex-exp 13110 ex-bc 13112 ex-gcd 13114 |
Copyright terms: Public domain | W3C validator |