bi2anan9 Show Code edit
# Deduction joining two equivalences to form equivalence of
# conjunctions.
## Join equivalences into equivalent conjunction
thm (bi2anan9 () (bi2an9.1 (-> ph (<-> ps ch)) bi2an9.2 (-> th (<-> ta et))) (-> (/\ ph th) (<-> (/\ ps ta) (/\ ch et))) bi2an9.1 ta anbi1d bi2an9.2 ch anbi2d sylan9bb)
(-> (/\ ph th) (<-> (/\ ps ta) (/\ ch et)))
edit