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

Proof

Step	Hyp	Ref	Expression
1		nnssi3.1	|- NN C_ D
2		nnssi3.2	|- ( C e. NN -> ph )
3		nnssi3.3	|- ( ( ( A e. D /\ B e. D /\ C e. D ) /\ ph ) -> ps )
4	1	sseli	|- ( A e. NN -> A e. D )
5	1	sseli	|- ( B e. NN -> B e. D )
6	1	sseli	|- ( C e. NN -> C e. D )
7	4 5 6	3anim123i	|- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A e. D /\ B e. D /\ C e. D ) )
8	2	3ad2ant3	|- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ph )
9	7 8 3	syl2anc	|- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ps )