# Metamath Proof Explorer

## Theorem nnssi3

Description: Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008)

Ref Expression
Hypotheses nnssi3.1 ${⊢}ℕ\subseteq {D}$
nnssi3.2 ${⊢}{C}\in ℕ\to {\phi }$
nnssi3.3 ${⊢}\left(\left({A}\in {D}\wedge {B}\in {D}\wedge {C}\in {D}\right)\wedge {\phi }\right)\to {\psi }$
Assertion nnssi3 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to {\psi }$

### Proof

Step Hyp Ref Expression
1 nnssi3.1 ${⊢}ℕ\subseteq {D}$
2 nnssi3.2 ${⊢}{C}\in ℕ\to {\phi }$
3 nnssi3.3 ${⊢}\left(\left({A}\in {D}\wedge {B}\in {D}\wedge {C}\in {D}\right)\wedge {\phi }\right)\to {\psi }$
4 1 sseli ${⊢}{A}\in ℕ\to {A}\in {D}$
5 1 sseli ${⊢}{B}\in ℕ\to {B}\in {D}$
6 1 sseli ${⊢}{C}\in ℕ\to {C}\in {D}$
7 4 5 6 3anim123i ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to \left({A}\in {D}\wedge {B}\in {D}\wedge {C}\in {D}\right)$
8 2 3ad2ant3 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to {\phi }$
9 7 8 3 syl2anc ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to {\psi }$