muleq12d Show Code edit
## Equality over Multiplication
thm (muleq12d ()
(hyp1 (-> ph (= A B))
hyp2 (-> ph (= C D)))
(-> ph (= (* A C) (* B D)))
hyp1 hyp2
(-> ph (= C D))
jca
(-> ph (/\ (= A B) (= C D)))
A B C D muleq12
(-> (/\ (= A B) (= C D)) (= (* A C) (* B D)))
syl
(-> ph (= (* A C) (* B D)))
)
edit