Axiom ax-L9-multl 25

Description: Left '⋅' substitution.

Assertion

Ref	Expression
ax-L9-multl	⊢ (𝑡 = 𝑢 → (𝑡 ⋅ 𝑤) = (𝑢 ⋅ 𝑤))

Detailed syntax breakdown of Axiom ax-L9-multl

Step	Hyp	Ref	Expression
1		term-t	. . 3 term 𝑡
2		term-u	. . 3 term 𝑢
3	1, 2	wff-equals 6	. 2 wff 𝑡 = 𝑢
4		term-w	. . . 4 term 𝑤
5	1, 4	term-mult 5	. . 3 term (𝑡 ⋅ 𝑤)
6	2, 4	term-mult 5	. . 3 term (𝑢 ⋅ 𝑤)
7	5, 6	wff-equals 6	. 2 wff (𝑡 ⋅ 𝑤) = (𝑢 ⋅ 𝑤)
8	3, 7	wff-imp 10	1 wff (𝑡 = 𝑢 → (𝑡 ⋅ 𝑤) = (𝑢 ⋅ 𝑤))

This axiom is referenced by:  submultl-P5  649  example-E6.02a  712