This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nnmcli

Description: _om is closed under multiplication. Inference form of nnmcl . (Contributed by Scott Fenton, 20-Apr-2012)

Ref Expression
Hypotheses nncli.1 ⊢ A ∈ ω
nncli.2 ⊢ B ∈ ω
Assertion nnmcli ⊢ A ⋅ 𝑜 B ∈ ω

Proof

Step Hyp Ref Expression
1 nncli.1 ⊢ A ∈ ω
2 nncli.2 ⊢ B ∈ ω
3 nnmcl ⊢ A ∈ ω ∧ B ∈ ω → A ⋅ 𝑜 B ∈ ω
4 1 2 3 mp2an ⊢ A ⋅ 𝑜 B ∈ ω