3orbi123d Show Code edit
# Deduction joining 3 equivalences to form equivalence of disjunctions.
thm (3orbi123d () (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 orbi12d bi3d.3 orbi12d ps th et df-3or ch ta ze df-3or 3bitr4g)
(-> ph (<-> (\/\/ ps th et) (\/\/ ch ta ze)))
edit