eqqeqq2i Show Code edit
thm (eqqeqq2i () (
hyp1 (= A B))
(<-> (= C A) (= C B))
hyp1
(= A B)
A B C eqqeqq2
(-> (= A B) (<-> (= C A) (= C B)))
ax-mp
(<-> (= C A) (= C B))
)
edit