Metamath Proof Explorer


Theorem nnacli

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

Ref Expression
Hypotheses nncli.1 A ω
nncli.2 B ω
Assertion nnacli A + 𝑜 B ω

Proof

Step Hyp Ref Expression
1 nncli.1 A ω
2 nncli.2 B ω
3 nnacl A ω B ω A + 𝑜 B ω
4 1 2 3 mp2an A + 𝑜 B ω