3anbi123d Show Code edit
# Deduction joining 3 equivalences to form equivalence of conjunctions.
thm (3anbi123d () (bi3d.1 (-> ph (<-> ps ch)) bi3d.2 (-> ph (<-> th ta)) bi3d.3 (-> ph (<-> et ze))) (-> ph (<-> (/\/\ ps th et) (/\/\ ch ta ze))) bi3d.1 bi3d.2 anbi12d bi3d.3 anbi12d ps th et df-3an ch ta ze df-3an 3bitr4g)
(-> ph (<-> (/\/\ ps th et) (/\/\ ch ta ze)))
edit