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	|- NN C_ D
	nnssi2.2	|- ( B e. NN -> ph )
	nnssi2.3	|- ( ( A e. D /\ B e. D /\ ph ) -> ps )
Assertion	nnssi2	|- ( ( A e. NN /\ B e. NN ) -> ps )

Proof

Step	Hyp	Ref	Expression
1		nnssi2.1	|- NN C_ D
2		nnssi2.2	|- ( B e. NN -> ph )
3		nnssi2.3	|- ( ( A e. D /\ B e. D /\ ph ) -> ps )
4	1	sseli	|- ( A e. NN -> A e. D )
5	1	sseli	|- ( B e. NN -> B e. D )
6	4 5 2	3anim123i	|- ( ( A e. NN /\ B e. NN /\ B e. NN ) -> ( A e. D /\ B e. D /\ ph ) )
7	6	3anidm23	|- ( ( A e. NN /\ B e. NN ) -> ( A e. D /\ B e. D /\ ph ) )
8	7 3	syl	|- ( ( A e. NN /\ B e. NN ) -> ps )