Theorem 4nn 9349

Description: 4 is a positive integer. (Contributed by NM, 8-Jan-2006.)

Assertion

Ref	Expression
4nn	⊢ 4 ∈ ℕ

Proof of Theorem 4nn

Step	Hyp	Ref	Expression
1		df-4 9246	. 2 ⊢ 4 = (3 + 1)
2		3nn 9348	. . 3 ⊢ 3 ∈ ℕ
3		peano2nn 9197	. . 3 ⊢ (3 ∈ ℕ → (3 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (3 + 1) ∈ ℕ
5	1, 4	eqeltri 2304	1 ⊢ 4 ∈ ℕ

Syntax hints:   ∈ wcel 2202  (class class class)co 6028  1c1 8076   + caddc 8078  ℕcn 9185  3c3 9237  4c4 9238

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-sep 4212  ax-cnex 8166  ax-resscn 8167  ax-1re 8169  ax-addrcl 8172

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-int 3934  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031  df-inn 9186  df-2 9244  df-3 9245  df-4 9246

This theorem is referenced by:  5nn  9350  4nn0  9463  4z  9553  fldiv4p1lem1div2  10611  fldiv4lem1div2uz2  10612  fldiv4lem1div2  10613  iexpcyc  10952  resqrexlemnmsq  11640  ef01bndlem  12380  flodddiv4  12560  flodddiv4t2lthalf  12563  6lcm4e12  12722  2expltfac  13075  starvndx  13285  starvid  13286  starvslid  13287  srngstrd  13292  homndx  13379  homid  13380  homslid  13381  prdsvalstrd  13417  dveflem  15520  tan4thpi  15635  gausslemma2dlem0d  15854  gausslemma2dlem3  15865  gausslemma2dlem4  15866  gausslemma2dlem5a  15867  gausslemma2dlem5  15868  gausslemma2dlem6  15869  m1lgs  15887  2lgslem1a2  15889  2lgslem1a  15890  2lgslem1  15893  2lgslem2  15894  2lgslem3a  15895  2lgslem3b  15896  2lgslem3c  15897  2lgslem3d  15898