3orbi123i Show Code edit
# Join 3 biconditionals with disjunction.
thm (3orbi123i () (bi3.1 (<-> ph ps) bi3.2 (<-> ch th) bi3.3 (<-> ta et)) (<-> (\/\/ ph ch ta) (\/\/ ps th et)) bi3.1 bi3.2 orbi12i bi3.3 orbi12i ph ch ta df-3or ps th et df-3or 3bitr4i)
(<-> (\/\/ ph ch ta) (\/\/ ps th et))
edit