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	⊢ ℕ ⊆ 𝐷
	nnssi3.2	⊢ ( 𝐶 ∈ ℕ → 𝜑 )
	nnssi3.3	⊢ ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷 ) ∧ 𝜑 ) → 𝜓 )
Assertion	nnssi3	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		nnssi3.1	⊢ ℕ ⊆ 𝐷
2		nnssi3.2	⊢ ( 𝐶 ∈ ℕ → 𝜑 )
3		nnssi3.3	⊢ ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷 ) ∧ 𝜑 ) → 𝜓 )
4	1	sseli	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ 𝐷 )
5	1	sseli	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ 𝐷 )
6	1	sseli	⊢ ( 𝐶 ∈ ℕ → 𝐶 ∈ 𝐷 )
7	4 5 6	3anim123i	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷 ) )
8	2	3ad2ant3	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝜑 )
9	7 8 3	syl2anc	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝜓 )