Metamath Proof Explorer


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 ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝜓 )