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	$$⊢\mathbb{N}\subseteq D$$
	nnssi2.2	$$⊢B\in \mathbb{N}\to \phi$$
	nnssi2.3	$$⊢\left(A\in D\wedge B\in D\wedge \phi \right)\to \psi$$
Assertion	nnssi2	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to \psi$$

Proof

Step	Hyp	Ref	Expression
1		nnssi2.1	$$⊢\mathbb{N}\subseteq D$$
2		nnssi2.2	$$⊢B\in \mathbb{N}\to \phi$$
3		nnssi2.3	$$⊢\left(A\in D\wedge B\in D\wedge \phi \right)\to \psi$$
4	1	sseli	$$⊢A\in \mathbb{N}\to A\in D$$
5	1	sseli	$$⊢B\in \mathbb{N}\to B\in D$$
6	4 5 2	3anim123i	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to \left(A\in D\wedge B\in D\wedge \phi \right)$$
7	6	3anidm23	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to \left(A\in D\wedge B\in D\wedge \phi \right)$$
8	7 3	syl	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to \psi$$