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 e. _om
nncli.2
|- B e. _om
Assertion nnmcli
|- ( A .o B ) e. _om

Proof

Step Hyp Ref Expression
1 nncli.1
 |-  A e. _om
2 nncli.2
 |-  B e. _om
3 nnmcl
 |-  ( ( A e. _om /\ B e. _om ) -> ( A .o B ) e. _om )
4 1 2 3 mp2an
 |-  ( A .o B ) e. _om