or23 Show Code edit
## Rearrangement of disjuncts
thm (or23 () () (<-> (\/ (\/ ph ps) ch) (\/ (\/ ph ch) ps))
ph ps orcom
(<-> (\/ ph ps) (\/ ps ph))
ch orbi1i
(<-> (\/ (\/ ph ps) ch) (\/ (\/ ps ph) ch))
ps ph ch orass
(<-> (\/ (\/ ps ph) ch) (\/ ps (\/ ph ch)))
bitri
(<-> (\/ (\/ ph ps) ch) (\/ ps (\/ ph ch)))
ps (\/ ph ch) orcom
(<-> (\/ ps (\/ ph ch)) (\/ (\/ ph ch) ps))
bitri
(<-> (\/ (\/ ph ps) ch) (\/ (\/ ph ch) ps))
)
edit