Metamath Proof Explorer

Theorem nmulr0d

Description: Natural multiplication by zero. Deduction form. (Contributed by Scott Fenton, 30-Jul-2026)

Ref Expression
Hypothesis nmul.1 
|- ( ph -> A e. On )
Assertion nmulr0d 
|- ( ph -> ( A .no (/) ) = (/) )

Proof

Step Hyp Ref Expression
1 nmul.1 
 |-  ( ph -> A e. On )
2 nmulr0 
 |-  ( A e. On -> ( A .no (/) ) = (/) )
3 1 2 syl 
 |-  ( ph -> ( A .no (/) ) = (/) )