muleq1d Show Code edit
## Equality over Multiplication
thm (muleq1d ()
(hyp (-> ph (= A B)))
(-> ph (= (* A C) (* B C)))
hyp C eqid A B C C muleq12 mpan2 syl
(-> ph (= (* A C) (* B C)))
)
edit