Metamath Proof Explorer


Theorem sn-mul01

Description: mul01 without ax-mulcom . (Contributed by SN, 5-May-2024)

Ref Expression
Assertion sn-mul01 A A 0 = 0

Proof

Step Hyp Ref Expression
1 id A A
2 0cnd A 0
3 1 2 mulcld A A 0
4 1 2 2 adddid A A 0 + 0 = A 0 + A 0
5 sn-00id 0 + 0 = 0
6 5 oveq2i A 0 + 0 = A 0
7 4 6 eqtr3di A A 0 + A 0 = A 0
8 3 7 sn-addid0 A A 0 = 0