pm1.4 Show Code edit
## Commutative Property of OR
thm (pm1.4 () () (-> (\/ ph ps) (\/ ps ph))
ph ps orcom
(<-> (\/ ph ps) (\/ ps ph))
biimpi
(-> (\/ ph ps) (\/ ps ph))
)
edit