or4 Show Code edit
## Rearrangement of disjuncts
thm (or4 () () (<-> (\/ (\/ ph ps) (\/ ch th)) (\/ (\/ ph ch) (\/ ps th)))
ph ps (\/ ch th) orass
(<-> (\/ (\/ ph ps) (\/ ch th)) (\/ ph (\/ ps (\/ ch th))))
ps ch th or12
(<-> (\/ ps (\/ ch th)) (\/ ch (\/ ps th)))
ph orbi2i
(<-> (\/ ph (\/ ps (\/ ch th))) (\/ ph (\/ ch (\/ ps th))))
bitri
(<-> (\/ (\/ ph ps) (\/ ch th)) (\/ ph (\/ ch (\/ ps th))))
ph ch (\/ ps th) orass
(<-> (\/ (\/ ph ch) (\/ ps th)) (\/ ph (\/ ch (\/ ps th))))
bicomi
(<-> (\/ ph (\/ ch (\/ ps th))) (\/ (\/ ph ch) (\/ ps th)))
bitri
(<-> (\/ (\/ ph ps) (\/ ch th)) (\/ (\/ ph ch) (\/ ps th)))
)
edit