an4 Show Code edit
## Rearrange Conjunction
thm (an4 () () (<-> (/\ (/\ ph ps) (/\ ch th)) (/\ (/\ ph ch) (/\ ps th))) ps ch th an12 ph anbi2i ph ps (/\ ch th) anass ph ch (/\ ps th) anass 3bitr4i)
(<-> (/\ (/\ ph ps) (/\ ch th)) (/\ (/\ ph ch) (/\ ps th)))
edit