Metamath Proof Explorer

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 ⊢ ℕ ⊆ D
nnssi3.2 ⊢ C ∈ ℕ → φ
nnssi3.3 ⊢ A ∈ D ∧ B ∈ D ∧ C ∈ D ∧ φ → ψ
Assertion nnssi3 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → ψ

Proof

Step Hyp Ref Expression
1 nnssi3.1 ⊢ ℕ ⊆ D
2 nnssi3.2 ⊢ C ∈ ℕ → φ
3 nnssi3.3 ⊢ A ∈ D ∧ B ∈ D ∧ C ∈ D ∧ φ → ψ
4 1 sseli ⊢ A ∈ ℕ → A ∈ D
5 1 sseli ⊢ B ∈ ℕ → B ∈ D
6 1 sseli ⊢ C ∈ ℕ → C ∈ D
7 4 5 6 3anim123i ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → A ∈ D ∧ B ∈ D ∧ C ∈ D
8 2 3ad2ant3 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → φ
9 7 8 3 syl2anc ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → ψ