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