muleq2d Show Code edit
thm (muleq2d () (
hyp1 (-> ph (= A B)))
(-> ph (= (* C A) (* C B)))
hyp1
(-> ph (= A B))
A B C muleq2
(-> (= A B) (= (* C A) (* C B)))
syl
(-> ph (= (* C A) (* C B)))
)
edit