3anbi123i Show Code edit
# Join 3 biconditionals with conjunction.
thm (3anbi123i () (bi3.1 (<-> ph ps) bi3.2 (<-> ch th) bi3.3 (<-> ta et)) (<-> (/\/\ ph ch ta) (/\/\ ps th et)) bi3.1 bi3.2 anbi12i bi3.3 anbi12i ph ch ta df-3an ps th et df-3an 3bitr4i)
(<-> (/\/\ ph ch ta) (/\/\ ps th et))
edit