Theorem nnssi2

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

	Ref	Expression
Hypotheses	nnssi2.1	⊢ ℕ ⊆ 𝐷
	nnssi2.2	⊢ ( 𝐵 ∈ ℕ → 𝜑 )
	nnssi2.3	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝜑 ) → 𝜓 )
Assertion	nnssi2	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		nnssi2.1	⊢ ℕ ⊆ 𝐷
2		nnssi2.2	⊢ ( 𝐵 ∈ ℕ → 𝜑 )
3		nnssi2.3	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝜑 ) → 𝜓 )
4	1	sseli	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ 𝐷 )
5	1	sseli	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ 𝐷 )
6	4 5 2	3anim123i	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝜑 ) )
7	6	3anidm23	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝜑 ) )
8	7 3	syl	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝜓 )