Metamath Proof Explorer

Theorem nnmulcld

Description: Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses nnge1d.1 φ A
nnmulcld.2 φ B
Assertion nnmulcld φ A B


Step Hyp Ref Expression
1 nnge1d.1 φ A
2 nnmulcld.2 φ B
3 nnmulcl A B A B
4 1 2 3 syl2anc φ A B