eqtr.4 Show Code edit
thm (eqtr.4 () () (-> (/\ (z.= (bottom B) (z.0)) (= A B)) (z.= (bottom A) (z.0)))
A B dfeq2
(-> (= A B) (<-> (z.= (bottom A) (z.0)) (z.= (bottom B) (z.0))))
(z.= (bottom B) (z.0)) anim2i
(-> (/\ (z.= (bottom B) (z.0)) (= A B)) (/\ (z.= (bottom B) (z.0)) (<-> (z.= (bottom A) (z.0)) (z.= (bottom B) (z.0)))))
## <d 'Infer Right to Left '>
(z.= (bottom A) (z.0)) (z.= (bottom B) (z.0)) bi2
(-> (<-> (z.= (bottom A) (z.0)) (z.= (bottom B) (z.0))) (-> (z.= (bottom B) (z.0)) (z.= (bottom A) (z.0))))
ImpReplaceImp1An1
(-> (/\ (z.= (bottom B) (z.0)) (= A B)) (/\ (z.= (bottom B) (z.0)) (-> (z.= (bottom B) (z.0)) (z.= (bottom A) (z.0)))))
## </d 'Infer Right to Left '>
## <d 'Introduce conjunct as antecedent '>
(z.= (bottom B) (z.0)) (z.= (bottom A) (z.0)) abai bicomi
(<-> (/\ (z.= (bottom B) (z.0)) (-> (z.= (bottom B) (z.0)) (z.= (bottom A) (z.0)))) (/\ (z.= (bottom B) (z.0)) (z.= (bottom A) (z.0))))
sylib
(-> (/\ (z.= (bottom B) (z.0)) (= A B)) (/\ (z.= (bottom B) (z.0)) (z.= (bottom A) (z.0))))
## </d 'Introduce conjunct as antecedent '>
## <d 'Remove Left Side of AND '>
(z.= (bottom B) (z.0)) (z.= (bottom A) (z.0)) pm3.27
(-> (/\ (z.= (bottom B) (z.0)) (z.= (bottom A) (z.0))) (z.= (bottom A) (z.0)))
syl
(-> (/\ (z.= (bottom B) (z.0)) (= A B)) (z.= (bottom A) (z.0)))
## </d 'Remove Left Side of AND '>
)
edit