![]() |
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 7826 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | addcomli.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | eqtri 2135 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1406 ax-gen 1408 ax-4 1470 ax-17 1489 ax-ext 2097 ax-addcom 7642 |
This theorem depends on definitions: df-bi 116 df-cleq 2108 |
This theorem is referenced by: negsubdi2i 7968 1p2e3 8755 peano2z 8991 4t4e16 9181 6t3e18 9187 6t5e30 9189 7t3e21 9192 7t4e28 9193 7t6e42 9195 7t7e49 9196 8t3e24 9198 8t4e32 9199 8t5e40 9200 8t8e64 9203 9t3e27 9205 9t4e36 9206 9t5e45 9207 9t6e54 9208 9t7e63 9209 9t8e72 9210 9t9e81 9211 4bc3eq4 10409 n2dvdsm1 11455 6gcd4e2 11526 ex-exp 12626 ex-bc 12628 ex-gcd 12630 |
Copyright terms: Public domain | W3C validator |