Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > addcomli | Unicode 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 7874 | . 2 |
4 | addcomli.2 | . 2 | |
5 | 3, 4 | eqtri 2138 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1316 wcel 1465 (class class class)co 5742 cc 7586 caddc 7591 |
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 1408 ax-gen 1410 ax-4 1472 ax-17 1491 ax-ext 2099 ax-addcom 7688 |
This theorem depends on definitions: df-bi 116 df-cleq 2110 |
This theorem is referenced by: negsubdi2i 8016 1p2e3 8822 peano2z 9058 4t4e16 9248 6t3e18 9254 6t5e30 9256 7t3e21 9259 7t4e28 9260 7t6e42 9262 7t7e49 9263 8t3e24 9265 8t4e32 9266 8t5e40 9267 8t8e64 9270 9t3e27 9272 9t4e36 9273 9t5e45 9274 9t6e54 9275 9t7e63 9276 9t8e72 9277 9t9e81 9278 4bc3eq4 10487 n2dvdsm1 11537 6gcd4e2 11610 eulerid 12810 cosq23lt0 12841 ex-exp 12866 ex-bc 12868 ex-gcd 12870 |
Copyright terms: Public domain | W3C validator |