eqtr.0 Show Code edit
thm (eqtr.0 () () (-> (/\ (= A B) (= B C)) (<-> (z.= (bottom A) (z.0)) (z.= (bottom C) (z.0))))
A B dfeq2
(-> (= A B) (<-> (z.= (bottom A) (z.0)) (z.= (bottom B) (z.0))))
B C dfeq2
(-> (= B C) (<-> (z.= (bottom B) (z.0)) (z.= (bottom C) (z.0))))
anim12i
(-> (/\ (= A B) (= B C)) (/\ (<-> (z.= (bottom A) (z.0)) (z.= (bottom B) (z.0))) (<-> (z.= (bottom B) (z.0)) (z.= (bottom C) (z.0)))))
## <d 'Transitive Property '>
(z.= (bottom A) (z.0)) (z.= (bottom B) (z.0)) (z.= (bottom C) (z.0)) bitr
(-> (/\ (<-> (z.= (bottom A) (z.0)) (z.= (bottom B) (z.0))) (<-> (z.= (bottom B) (z.0)) (z.= (bottom C) (z.0)))) (<-> (z.= (bottom A) (z.0)) (z.= (bottom C) (z.0))))
syl
(-> (/\ (= A B) (= B C)) (<-> (z.= (bottom A) (z.0)) (z.= (bottom C) (z.0))))
## </d 'Transitive Property '>
)
edit