Theorem 3nn0 9157

Description: 3 is a nonnegative integer. (Contributed by Mario Carneiro, 18-Feb-2014.)

Assertion

Ref	Expression
3nn0	|- 3 e. NN0

Proof of Theorem 3nn0

Step	Hyp	Ref	Expression
1		3nn 9044	. 2 |- 3 e. NN
2	1	nnnn0i 9147	1 |- 3 e. NN0

Syntax hints:   e. wcel 2142   3c3 8934   NN0cn0 9139

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 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-ext 2153  ax-sep 4108  ax-cnex 7869  ax-resscn 7870  ax-1re 7872  ax-addrcl 7875

This theorem depends on definitions:  df-bi 116  df-3an 976  df-tru 1352  df-nf 1455  df-sb 1757  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-ral 2454  df-rex 2455  df-v 2733  df-un 3126  df-in 3128  df-ss 3135  df-sn 3590  df-pr 3591  df-op 3593  df-uni 3798  df-int 3833  df-br 3991  df-iota 5162  df-fv 5208  df-ov 5860  df-inn 8883  df-2 8941  df-3 8942  df-n0 9140

This theorem is referenced by:  7p4e11  9422  7p7e14  9425  8p4e12  9428  8p6e14  9430  9p4e13  9435  9p5e14  9436  4t4e16  9445  5t4e20  9448  6t4e24  9452  6t6e36  9454  7t4e28  9457  7t6e42  9459  8t4e32  9463  8t5e40  9464  9t4e36  9470  9t5e45  9471  9t7e63  9473  9t8e72  9474  fz0to3un2pr  10083  4fvwrd4  10100  fldiv4p1lem1div2  10265  expnass  10585  binom3  10597  fac4  10671  4bc2eq6  10712  ef4p  11661  efi4p  11684  resin4p  11685  recos4p  11686  ef01bndlem  11723  sin01bnd  11724  sin01gt0  11728  tangtx  13638  binom4  13776