df-3an Show Code edit
defthm (df-3an wff (/\/\ ph ps ch) () () (<-> (/\/\ ph ps ch) (/\ (/\ ph ps) ch))
(/\ (/\ ph ps) ch) biid)
(<-> (/\ (/\ ph ps) ch) (/\ (/\ ph ps) ch))
edit