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