Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 8nn0 | Unicode version |
Description: 8 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) |
Ref | Expression |
---|---|
8nn0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 8nn 9001 | . 2 | |
2 | 1 | nnnn0i 9099 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 2128 c8 8891 cn0 9091 |
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-io 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2139 ax-sep 4083 ax-cnex 7824 ax-resscn 7825 ax-1re 7827 ax-addrcl 7830 |
This theorem depends on definitions: df-bi 116 df-3an 965 df-tru 1338 df-nf 1441 df-sb 1743 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-ral 2440 df-rex 2441 df-v 2714 df-un 3106 df-in 3108 df-ss 3115 df-sn 3566 df-pr 3567 df-op 3569 df-uni 3774 df-int 3809 df-br 3967 df-iota 5136 df-fv 5179 df-ov 5828 df-inn 8835 df-2 8893 df-3 8894 df-4 8895 df-5 8896 df-6 8897 df-7 8898 df-8 8899 df-n0 9092 |
This theorem is referenced by: 8p3e11 9376 8p4e12 9377 8p5e13 9378 8p6e14 9379 8p7e15 9380 8p8e16 9381 9p9e18 9389 6t4e24 9401 7t5e35 9407 8t3e24 9411 8t4e32 9412 8t5e40 9413 8t6e48 9414 8t7e56 9415 8t8e64 9416 9t3e27 9418 9t9e81 9424 ex-exp 13345 |
Copyright terms: Public domain | W3C validator |