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

Metamath Proof Explorer

Theorem nnacli

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

Step	Hyp	Ref	Expression
1		nncli.1	$⊢ A \in ω$
2		nncli.2	$⊢ B \in ω$
3		nnacl	$⊢ (A \in ω \land B \in ω) \to A +_{𝑜} B \in ω$
4	1 2 3	mp2an	$⊢ A +_{𝑜} B \in ω$