an6 Show Code edit
# Rearrangement of 6 conjuncts.
thm (an6 () () (<-> (/\ (/\/\ ph ps ch) (/\/\ th ta et)) (/\/\ (/\ ph th) (/\ ps ta) (/\ ch et))) ph ps ch df-3an th ta et df-3an anbi12i (/\ ph ps) ch (/\ th ta) et an4 ph ps th ta an4 (/\ ch et) anbi1i 3bitri (/\ ph th) (/\ ps ta) (/\ ch et) df-3an bitr4i)
(<-> (/\ (/\/\ ph ps ch) (/\/\ th ta et)) (/\/\ (/\ ph th) (/\ ps ta) (/\ ch et)))
edit