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

Metamath Proof Explorer

Theorem nnm0

Description: Multiplication with zero. Theorem 4J(A1) of Enderton p. 80. (Contributed by NM, 20-Sep-1995)

		Ref	Expression
	Assertion	nnm0	$⊢ A \in ω \to A \cdot_{𝑜} \emptyset = \emptyset$

Step	Hyp	Ref	Expression
1		nnon	$⊢ A \in ω \to A \in On$
2		om0	$⊢ A \in On \to A \cdot_{𝑜} \emptyset = \emptyset$
3	1 2	syl	$⊢ A \in ω \to A \cdot_{𝑜} \emptyset = \emptyset$