pm2.31 Show Code edit
## Associatative Property of OR
thm (pm2.31 () () (-> (\/ ph (\/ ps ch)) (\/ (\/ ph ps) ch))
ph ps ch orass
(<-> (\/ (\/ ph ps) ch) (\/ ph (\/ ps ch)))
biimpri
(-> (\/ ph (\/ ps ch)) (\/ (\/ ph ps) ch))
)
edit