Metamath Proof Explorer
Description: Multiplication by 0 . Theorem I.6 of Apostol p. 18. (Contributed by NM, 23Nov1994) (Revised by Scott Fenton, 3Jan2013)


Ref 
Expression 

Hypothesis 
mul.1 
$${\u22a2}{A}\in \u2102$$ 

Assertion 
mul01i 
$${\u22a2}{A}\cdot 0=0$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

mul.1 
$${\u22a2}{A}\in \u2102$$ 
2 

mul01 
$${\u22a2}{A}\in \u2102\to {A}\cdot 0=0$$ 
3 
1 2

axmp 
$${\u22a2}{A}\cdot 0=0$$ 