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 |
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 |