Metamath Proof Explorer

Theorem nmull0d

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

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

Proof

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