eqqeqq1 Show Code edit
thm (eqqeqq1 () () (-> (= A B) (<-> (= A C) (= B C)))
B A C eqtr ex
(-> (= B A) (-> (= A C) (= B C)))
B A eqcom
(<-> (= B A) (= A B))
sylbi2
(-> (= A B) (-> (= A C) (= B C)))
A B C eqtr ex
(-> (= A B) (-> (= B C) (= A C)))
impbid
(-> (= A B) (<-> (= A C) (= B C)))
)
edit