Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pinn Structured version   Unicode version

Theorem pinn 9304
 Description: A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
Assertion
Ref Expression
pinn

Proof of Theorem pinn
StepHypRef Expression
1 df-ni 9298 . . 3
2 difss 3592 . . 3
31, 2eqsstri 3494 . 2
43sseli 3460 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wcel 1868   cdif 3433  c0 3761  csn 3996  com 6703  cnpi 9270 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400 This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-v 3083  df-dif 3439  df-in 3443  df-ss 3450  df-ni 9298 This theorem is referenced by:  pion  9305  piord  9306  mulidpi  9312  addclpi  9318  mulclpi  9319  addcompi  9320  addasspi  9321  mulcompi  9322  mulasspi  9323  distrpi  9324  addcanpi  9325  mulcanpi  9326  addnidpi  9327  ltexpi  9328  ltapi  9329  ltmpi  9330  indpi  9333
 Copyright terms: Public domain W3C validator